for a, b being Nat st a gcd b = 1 holds
(a + b) gcd b = 1