theorem MOS8: :: NEWTON06:59

for i being Integer holds
( (i |^ 2) mod 8 = 0 or (i |^ 2) mod 8 = 1 or (i |^ 2) mod 8 = 4 )