theorem :: NUMBER04:5
for k, n being Nat st k is odd holds
(- 1) |^ k, - 1 are_congruent_mod n by INT_1:11;