for a, b being Nat
for x being Integer st a <> 0 holds
(a + (x * b)) gcd b = a gcd b