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