let m, n be Nat; :: thesis: m gcd (m lcm n) = m
set M = m lcm n;
( m divides m lcm n & n divides m lcm n & ( for k being Nat st m divides k & n divides k holds
m lcm n divides k ) ) by NAT_D:def 4;
hence m gcd (m lcm n) = m by Th62; :: thesis: verum