for a, b being Integer st b <> 0 holds
a mod b,a are_congruent_mod b