let i, j be Integer; :: thesis: ( i,j are_congruent_mod j implies j divides i )
assume i,j are_congruent_mod j ; :: thesis: j divides i
then consider k being Integer such that
A1: i = (k * j) + j by NAT_6:9;
i = j * (k + 1) by A1;
hence j divides i ; :: thesis: verum