let i1, i2 be Integer; :: thesis: i1,i1 are_congruent_mod i2
i2 * 0 = i1 - i1 ;
hence i1,i1 are_congruent_mod i2 ; :: thesis: verum