theorem Th37: :: NUMBER05:41

for n being Nat st n is odd holds
(n ^2) mod 8 = 1