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
consider l being Nat such that
A3: j = i * l by A2, Lm7;
l <> 0 by A1, A3;
then consider k being Nat such that
A4: l = k + 1 by NAT_1:6;
i * (k + 1) = i + (i * k) ;
hence i <= j by A3, A4, NAT_1:11; :: thesis: verum