let n, m 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:80
.= (m div n) * n ;
hence n divides m by INT_1:def 9; :: thesis: verum