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

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