let i1, i2, i5 be Integer; :: thesis: ( i1,i2 are_congruent_mod i5 iff i1 - i5,i2 are_congruent_mod i5 )
thus ( i1,i2 are_congruent_mod i5 implies i1 - i5,i2 are_congruent_mod i5 ) :: thesis: ( i1 - i5,i2 are_congruent_mod i5 implies i1,i2 are_congruent_mod i5 )

proof

assume i1,i2 are_congruent_mod i5 ; :: thesis: i1 - i5,i2 are_congruent_mod i5
then consider i0 being Integer such that
A1: i5 * i0 = i1 - i2 ;
i5 * (i0 - 1) = (i1 - i5) - i2 by A1;
hence i1 - i5,i2 are_congruent_mod i5 ; :: thesis: verum

end;

assume i1 - i5,i2 are_congruent_mod i5 ; :: thesis: i1,i2 are_congruent_mod i5
then consider i0 being Integer such that
A2: i5 * i0 = (i1 - i5) - i2 ;
i5 * (i0 + 1) = i1 - i2 by A2;
hence i1,i2 are_congruent_mod i5 ; :: thesis: verum