theorem :: NEWTON07:29

for a, b being Nat holds (((a * b) + 1) choose 1) mod b = 1 mod b