theorem :: NEWTON06:34

for a, b being odd Nat st a,b are_coprime & ((a |^ 2) + (b |^ 2)) / 2 is square holds
not 3 divides a * b