for a, b being Nat st a <> 0 & b <> 0 holds
ex c, d being Nat st a gcd b = (a * c) - (b * d)