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 A2: ( l < j & 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 A2; :: thesis: verum