let n, m be Nat; :: thesis: (m gcd n) lcm n = n
set M = m gcd n;
m gcd n divides n by NAT_D:def 5;
hence (m gcd n) lcm n = n by Th44; :: thesis: verum