let a, b be Nat; :: thesis: ( a > b & a,b are_coprime implies (a + b) gcd (a - b) <= 2 )
assume A1: ( a > b & a,b are_coprime ) ; :: thesis: (a + b) gcd (a - b) <= 2
then consider c being Nat such that
A2: a = b + c by NAT_1:10;
c + (1 * b),b are_coprime by A1, A2;
then c,b are_coprime by Th5;
then ((2 * b) + c) gcd c <= 2 by Lm5;
hence (a + b) gcd (a - b) <= 2 by A2; :: thesis: verum