let k, n, m be Nat; :: thesis: m gcd (n gcd k) = (m gcd n) gcd k
set M = n gcd k;
set K = m gcd (n gcd k);
set N = m gcd n;
set L = (m gcd n) gcd k;
A1: m gcd (n gcd k) divides n gcd k by NAT_D:def 5;
A2: m gcd (n gcd k) divides m by NAT_D:def 5;
n gcd k divides n by NAT_D:def 5;
then m gcd (n gcd k) divides n by A1, NAT_D:4;
then A3: m gcd (n gcd k) divides m gcd n by A2, NAT_D:def 5;
A4: (m gcd n) gcd k divides m gcd n by NAT_D:def 5;
A5: (m gcd n) gcd k divides k by NAT_D:def 5;
m gcd n divides n by NAT_D:def 5;
then (m gcd n) gcd k divides n by A4, NAT_D:4;
then A6: (m gcd n) gcd k divides n gcd k by A5, NAT_D:def 5;
m gcd n divides m by NAT_D:def 5;
then (m gcd n) gcd k divides m by A4, NAT_D:4;
then A7: (m gcd n) gcd k divides m gcd (n gcd k) by A6, NAT_D:def 5;
n gcd k divides k by NAT_D:def 5;
then m gcd (n gcd k) divides k by A1, NAT_D:4;
then m gcd (n gcd k) divides (m gcd n) gcd k by A3, NAT_D:def 5;
hence m gcd (n gcd k) = (m gcd n) gcd k by A7, NAT_D:5; :: thesis: verum