:: deftheorem defines is_quadratic_residue_mod INT_5:def 2 :
for a being Integer
for m being natural Number holds
( a is_quadratic_residue_mod m iff ex x being Integer st ((x ^2) - a) mod m = 0 );