let n, m be Nat; :: thesis: ( m divides n iff m lcm n = n )
thus ( m divides n implies m lcm n = n ) :: thesis: ( m lcm n = n implies m divides n )

proof

set M = m lcm n;
assume m divides n ; :: thesis: m lcm n = n
then A1: m lcm n divides n by NAT_D:def 4;
n divides m lcm n by NAT_D:def 4;
hence m lcm n = n by A1, NAT_D:5; :: thesis: verum

end;

thus ( m lcm n = n implies m divides n ) by NAT_D:def 4; :: thesis: verum