theorem :: NEWTON06:55

for a, b, c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2 holds
( (b |^ 2) mod a = (c |^ 2) mod a & (a |^ 2) mod b = (c |^ 2) mod b )