theorem Th7: :: EULER_1:7

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