theorem Th36: :: NUMBER05:40

for n being Nat holds (((2 * n) + 1) ^2) mod 8 = 1