let n, m be Nat; :: thesis: m lcm n divides m * n
set s = m * n;
A1: n divides m * n by NAT_D:9;
m divides m * n by NAT_D:9;
hence m lcm n divides m * n by A1, NAT_D:def 4; :: thesis: verum