theorem NPP: :: NEWTON07:13

for n being Nat
for m being non zero Nat holds (n mod m) choose (m - 1) < 2