for p being natural prime number
for x being integer number holds
( x |^ 2,1 are_congruent_mod p iff ( x,1 are_congruent_mod p or x, - 1 are_congruent_mod p ) )