let k, n, m be Nat; :: thesis: ( m divides n implies k gcd m divides k gcd n )
set M = k gcd m;
A1: k gcd m divides k by NAT_D:def 5;
assume A2: m divides n ; :: thesis: k gcd m divides k gcd n
k gcd m divides m by NAT_D:def 5;
then k gcd m divides n by A2, NAT_D:4;
hence k gcd m divides k gcd n by A1, NAT_D:def 5; :: thesis: verum