let p be Prime; :: thesis: for k, n being Nat st k < n & n <= p holds
((p + n) choose k) mod p = (n choose k) mod p
let k, n be Nat; :: thesis: ( k < n & n <= p implies ((p + n) choose k) mod p = (n choose k) mod p )
assume A1: ( k < n & n <= p ) ; :: thesis: ((p + n) choose k) mod p = (n choose k) mod p

per cases ( not k is zero or k is zero ) ;

suppose not k is zero ; :: thesis: ((p + n) choose k) mod p = (n choose k) mod p

then reconsider k = k as non zero Nat ;

per cases ( n = p or n < p ) by A1, XXREAL_0:1;

suppose B1: n = p ; :: thesis: ((p + n) choose k) mod p = (n choose k) mod p

((2 * p) choose k) mod p = 0 by A1, B1, PCN;
hence ((p + n) choose k) mod p = (n choose k) mod p by A1, B1, PCK; :: thesis: verum

end;

suppose n < p ; :: thesis: ((p + n) choose k) mod p = (n choose k) mod p

hence ((p + n) choose k) mod p = (n choose k) mod p by A1, PCM; :: thesis: verum

end;

end;

end;

suppose k is zero ; :: thesis: ((p + n) choose k) mod p = (n choose k) mod p

then ( n choose k = 1 & (p + n) choose k = 1 ) by NEWTON:19;
hence ((p + n) choose k) mod p = (n choose k) mod p ; :: thesis: verum

end;

end;