theorem PCN: :: NEWTON07:25

for p being Prime
for n being non zero Nat st n < p holds
((2 * p) choose n) mod p = 0