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

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