let p be Prime; :: thesis: for n being Nat
for k being non zero Nat st n + k < p holds
((p + n) choose (k + n)) mod p = 0
defpred S₁[ Nat] means for k being non zero Nat st k + $1 < p holds
((p + $1) choose (k + $1)) mod p = 0 ;
A2: S₁[ 0 ] by PCK;
A3: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume B1: for k being non zero Nat st k + m < p holds
((p + m) choose (k + m)) mod p = 0 ; :: thesis: S₁[m + 1]
for k being non zero Nat st k + (m + 1) < p holds
((p + (m + 1)) choose (k + (m + 1))) mod p = 0

proof

let k be non zero Nat; :: thesis: ( k + (m + 1) < p implies ((p + (m + 1)) choose (k + (m + 1))) mod p = 0 )
assume C1: k + (m + 1) < p ; :: thesis: ((p + (m + 1)) choose (k + (m + 1))) mod p = 0
(k + m) + 0 < (k + m) + 1 by XREAL_1:6;
then C2: k + m < p by C1, XXREAL_0:2;
C3: ((p + m) choose (m + (k + 1))) mod p = 0 by C1, B1;
(((p + m) + 1) choose ((k + m) + 1)) mod p = (((p + m) choose (k + m)) + ((p + m) choose ((k + m) + 1))) mod p by NEWTON:22
.= ((((p + m) choose (k + m)) mod p) + (((p + m) choose ((k + m) + 1)) mod p)) mod p by NAT_D:66
.= (0 + 0) mod p by B1, C2, C3 ;
hence ((p + (m + 1)) choose (k + (m + 1))) mod p = 0 ; :: thesis: verum

end;

hence S₁[m + 1] ; :: thesis: verum

end;

for c being Nat holds S₁[c] from NAT_1:sch 2(A2, A3);
hence for n being Nat
for k being non zero Nat st n + k < p holds
((p + n) choose (k + n)) mod p = 0 ; :: thesis: verum