for a, b being Nat st a > b & a,b are_coprime holds
(a + b) gcd (a - b) <= 2