let i, j be Nat; :: thesis: ( 0 < j & i divides j implies i <= j )
assume that
A1: 0 < j and
A2: i divides j ; :: thesis: i <= j
A3: j = i * (j div i) by A2, Th3;
then j div i <> 0 by A1;
then consider m being Nat such that
A4: j div i = m + 1 by NAT_1:6;
i * (m + 1) = i + (i * m) ;
hence i <= j by A3, A4, NAT_1:11; :: thesis: verum