for n being natural number holds
( - 1,1 are_congruent_mod n iff ( n = 2 or n = 1 ) )