let m, n be Integer; :: thesis: ( n <> 0 & m mod n = 0 implies n divides m )
assume ( n <> 0 & m mod n = 0 ) ; :: thesis: n divides m
then m = ((m div n) * n) + 0 by NEWTON:66
.= (m div n) * n ;
hence n divides m ; :: thesis: verum