for i, x, y being Integer st x <> 0 & i >= 0 holds
(i * x) gcd (i * y) = i * (x gcd y)