let k be Nat; :: thesis: k,k + 1 are_relative_prime
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_relative_prime by INT_2:def 3; :: thesis: verum