theorem Th8: :: EULER_1:8
for a, b, c being Nat holds (a + (b * c)) gcd b = a gcd b