let p be Prime; :: thesis: ((2 * p) choose p) mod p = 2 mod p
reconsider n = p - 1 as Nat ;
n + 0 < n + 1 by XREAL_1:6;
then ( (((1 * p) + n) choose n) mod p = 1 & (((1 * p) + n) choose (1 * p)) mod p = 1 ) by NPK, KPN;
then 2 mod p = ((((p + n) choose n) mod p) + (((p + n) choose p) mod p)) mod p
.= (((p + n) choose n) + ((p + n) choose p)) mod p by NAT_D:66
.= (((p + n) + 1) choose (n + 1)) mod p by NEWTON:22 ;
hence ((2 * p) choose p) mod p = 2 mod p ; :: thesis: verum