let i1, i2 be Integer; :: thesis: i1,i2 are_congruent_mod 1
i1 - i2 = 1 * (i1 - i2) ;
hence i1,i2 are_congruent_mod 1 ; :: thesis: verum