let a, b, c be Nat; :: thesis: ( a + b divides c & a,c are_coprime implies a,b are_coprime )
assume A1: ( a + b divides c & a,c are_coprime ) ; :: thesis: a,b are_coprime
then consider k being Nat such that
A2: c = (a + b) * k by NAT_D:def 3;
1 = a gcd ((b * k) + (k * a)) by A1, A2
.= a gcd (b * k) by Th5 ;
then a * 1,k * b are_coprime ;
hence a,b are_coprime by NEWTON01:41; :: thesis: verum