let i, j be Integer; :: thesis: ( i divides j implies i,j - 1 are_coprime )
assume A1: i divides j ; :: thesis: i,j - 1 are_coprime
A2: ( 1 divides i & 1 divides j - 1 ) by INT_2:12;
for m being Integer st m divides i & m divides j - 1 holds
m divides 1

proof

let m be Integer; :: thesis: ( m divides i & m divides j - 1 implies m divides 1 )
assume m divides i ; :: thesis: ( not m divides j - 1 or m divides 1 )
then A3: m divides j by A1, INT_2:9;
assume m divides j - 1 ; :: thesis: m divides 1
then m divides (j - 1) - j by A3, INT_5:1;
then ( m = 1 or m = - 1 ) by INT_2:13;
hence m divides 1 by INT_2:14; :: thesis: verum

end;

hence i gcd (j - 1) = 1 by A2, INT_2:def 2; :: according to INT_2:def 3 :: thesis: verum