for p being natural positive number
for a being integer number holds
( a is_quadratic_residue_mod p iff ex x being integer number st x |^ 2,a are_congruent_mod p )