theorem :: NEWTON02:63

for a, b being Nat st a is odd & b is odd holds
8 divides (a |^ 2) - (b |^ 2)