let p be Prime; :: thesis: for n being Nat holds ((p * n) choose p) mod p = n mod p
let n be Nat; :: thesis: ((p * n) choose p) mod p = n mod p

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

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

hence ((p * n) choose p) mod p = n mod p ; :: thesis: verum

end;

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

then reconsider n = n as non zero Nat ;
( ((n * p) + 0) mod p = 0 mod p & ((1 * p) + 0) mod p = 0 mod p & ((n * p) + 0) div p = (0 div p) + n & ((1 * p) + 0) div p = (0 div p) + 1 ) by NAT_D:61;
then ((p * n) choose p) mod p = ((0 choose 0) * (n choose 1)) mod p by AL
.= (1 * n) mod p by NEWTON:21 ;
hence ((p * n) choose p) mod p = n mod p ; :: thesis: verum

end;

end;