theorem Th23: :: NUMBER15:23
for m being Nat st m is even holds
(3 |^ m) mod 4 = 1