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