let i, j be Integer; :: thesis: ( i,j are_coprime implies ex s being Integer st s * i,1 are_congruent_mod j )
assume i gcd j = 1 ; :: according to INT_2:def 3 :: thesis: ex s being Integer st s * i,1 are_congruent_mod j
then consider s, t being Integer such that
A1: 1 = (s * i) + (t * j) by NAT_D:68;
take s ; :: thesis: s * i,1 are_congruent_mod j
(s * i) - 1 = (- t) * j by A1;
then j divides (s * i) - 1 by INT_1:def 3;
hence s * i,1 are_congruent_mod j by INT_2:15; :: thesis: verum