theorem :: NEWTON06:58
for i being Integer holds
( (i |^ 2) mod 4 = 0 or (i |^ 2) mod 4 = 1 )