theorem :: NEWTON06:52

for a, b being non zero Nat st (a |^ 2) - (b |^ 2) in NAT holds
((a |^ 2) - (b |^ 2)) mod (2 * b) = ((a |^ 2) + (b |^ 2)) mod (2 * b)