let i, j, k, l be Nat; :: thesis: ( i = (j * k) + l & l < j & 0 < l implies not j divides i )
assume A1: i = (j * k) + l ; :: thesis: ( not l < j or not 0 < l or not j divides i )
assume that
A2: l < j and
A3: 0 < l ; :: thesis: not j divides i
assume j divides i ; :: thesis: contradiction
then i = j * (i div j) by NAT_D:3;
then j * (i div j) = (j * (i div j)) + l by A1, A2, NAT_D:def 1;
hence contradiction by A3; :: thesis: verum