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

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