theorem IPN: :: NEWTON07:41

for k being non zero Nat
for i being Nat
for p being Prime holds (((i * p) + (p -' k)) choose (p -' k)) mod p = 1