theorem Th9: :: NAT_4:9

for i, j, k, l being Nat st i = (j * k) + l & l < j & 0 < l holds
not j divides i