theorem NPR: :: NEWTON07:14

for n being Nat
for m being non zero Nat holds
( (n mod m) choose (m - 1) = 1 iff n mod m = m - 1 )