theorem :: NEWTON06:36
for a, b being square Nat st a,b are_coprime & (a - b) / 2 is square holds
b mod 3 = 1