theorem Th16: :: NAT_1:16

for n, k being natural Number st k <> 0 holds
n < n + k