let a, b, k be Nat; :: thesis: ( k > 0 & a + b > k & a + b divides k * a implies not a,b are_coprime )
assume A1: ( k > 0 & a + b > k & a + b divides k * a ) ; :: thesis: not a,b are_coprime

per cases ( b > 0 or b = 0 ) ;

suppose B1: b > 0 ; :: thesis: not a,b are_coprime

B2: not a + b,a are_coprime by A1, INT_2:25, INT_2:27;
assume a,b are_coprime ; :: thesis: contradiction
then 1 = (b + (1 * a)) gcd a by B1, EULER_1:16;
hence contradiction by B2; :: thesis: verum

end;

suppose b = 0 ; :: thesis: not a,b are_coprime

hence not a,b are_coprime by A1, NAT_1:14; :: thesis: verum

end;

end;