theorem :: NEWTON07:40
for p being Prime
for n being Nat holds (n choose (p - 1)) mod p = ((n mod p) choose (p - 1)) mod p