theorem Th9: :: NAT_4:9

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