for i1, i2 being Integer holds i1,i2 are_congruent_mod 1