theorem :: NEWTON06:83
for k being Integer holds
( ex a, b being Integer st (a |^ 2) - (b |^ 2) = k iff k mod 4 <> 2 )