theorem :: NEWTON07:39

for p being Prime holds ((2 * p) choose p) mod p = 2 mod p