let m, n 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 A1: m divides n ; :: thesis: m lcm n = n
A2: ( m divides m lcm n & n divides m lcm n & ( for s being Nat st m divides s & n divides s holds
m lcm n divides s ) ) by NAT_D:def 4;
m lcm n = n

proof

m lcm n divides n by A1, NAT_D:def 4;
hence m lcm n = n by A2, NAT_D:5; :: thesis: verum

end;

hence m lcm n = n ; :: thesis: verum

end;

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