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