let m, n be Nat; :: thesis: ( 0 < m & m * n divides m implies n = 1 )
assume that
A1: 0 < m and
A2: m * n divides m ; :: thesis: n = 1
m divides m * n ;
then ( m = m * n or m = - (m * n) ) by A2, INT_2:11;
hence n = 1 by A1, XCMPLX_1:7; :: thesis: verum