theorem :: INT_1:60

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