for i being integer Number holds
( - 1,1 are_congruent_mod i iff ( i = 2 or i = 1 or i = - 2 or i = - 1 ) )