theorem :: NEWTON02:27

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