for a being Integer
for m being Nat holds a ^2 is_quadratic_residue_mod m