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