let k be Nat; :: thesis: k,k + 1 are_coprime
k gcd (k + 1) = (1 + (k * 1)) gcd k
.= 1 gcd k by EULER_1:8
.= 1 by NEWTON:51 ;
hence k,k + 1 are_coprime by INT_2:def 3; :: thesis: verum