let i, j, k be Integer; :: thesis: ( i > 0 & j,k are_congruent_mod i implies ( i divides j iff i divides k ) )
assume A1: i > 0 ; :: thesis: ( not j,k are_congruent_mod i or ( i divides j iff i divides k ) )
assume j,k are_congruent_mod i ; :: thesis: ( i divides j iff i divides k )
then A2: j mod i = k mod i by NAT_D:64;
thus ( i divides j implies i divides k ) :: thesis: ( i divides k implies i divides j )

proof

assume i divides j ; :: thesis: i divides k
then j mod i = 0 by A1, INT_1:62;
hence i divides k by A1, A2, INT_1:62; :: thesis: verum

end;

assume i divides k ; :: thesis: i divides j
then k mod i = 0 by A1, INT_1:62;
hence i divides j by A1, A2, INT_1:62; :: thesis: verum