let p be Prime; :: thesis: for n being Nat holds ((p + n) choose p) mod p = ((n div p) + 1) mod p
let n be Nat; :: thesis: ((p + n) choose p) mod p = ((n div p) + 1) mod p
( ((1 * p) + n) mod p = n mod p & ((1 * p) + 0) mod p = 0 mod p & ((1 * p) + n) div p = (n div p) + 1 & ((1 * p) + 0) div p = (0 div p) + 1 ) by NAT_D:61;
then ((p + n) choose p) mod p = (((n mod p) choose 0) * ((1 + (n div p)) choose 1)) mod p by AL
.= (1 * ((n div p) + 1)) mod p by NEWTON:19 ;
hence ((p + n) choose p) mod p = ((n div p) + 1) mod p ; :: thesis: verum