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;
hence m divides 1 ; :: thesis: verum

end;

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