theorem Th51: :: NUMBER09:51

for n being Nat holds
( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 )