for m, j being Integer holds m * j, 0 are_congruent_mod m ;