let m, n 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 Th62; :: thesis: verum