let k be Integer; :: thesis: (2 * k) + 1,(9 * k) + 4 are_coprime
thus ((2 * k) + 1) gcd ((9 * k) + 4) = ((2 * k) + 1) gcd (((9 * k) + 4) - (4 * ((2 * k) + 1))) by NEWTON02:5
.= 1 gcd k by NEWTON02:5
.= 1 ; :: according to INT_2:def 3 :: thesis: verum