let k be Integer; :: thesis: ((2 * k) - 1) gcd ((9 * k) + 4) = (k + 8) gcd 17
thus ((2 * k) - 1) gcd ((9 * k) + 4) = ((2 * k) - 1) gcd (((9 * k) + 4) - (4 * ((2 * k) - 1))) by NEWTON02:5
.= (((2 * k) - 1) - (2 * (k + 8))) gcd (k + 8) by NEWTON02:5
.= (- 17) gcd (k + 8)
.= (k + 8) gcd 17 by NEWTON02:1 ; :: thesis: verum