theorem :: NEWTON06:75

for a being Integer holds (a |^ 4) mod 8 is trivial Nat