let a, b, k be Nat; :: thesis: ( k > 0 implies a gcd b <= a gcd (b * k) )
assume k > 0 ; :: thesis: a gcd b <= a gcd (b * k)
then ( b * k = 0 iff b = 0 ) ;
then A1: ( a gcd (b * k) = 0 implies a gcd b = 0 ) by INT_2:5;
A2: ( a gcd b divides b & a gcd b divides a ) by INT_2:def 2;
then a gcd b divides b * k by INT_2:2;
hence a gcd b <= a gcd (b * k) by A1, A2, INT_2:22, INT_2:27; :: thesis: verum