let p be Prime; :: thesis: for n, k being Nat st k <> p holds
(((n mod p) + 1) choose k) mod p = (((n + 1) mod p) choose k) mod p
let n, k be Nat; :: thesis: ( k <> p implies (((n mod p) + 1) choose k) mod p = (((n + 1) mod p) choose k) mod p )
assume A0: k <> p ; :: thesis: (((n mod p) + 1) choose k) mod p = (((n + 1) mod p) choose k) mod p
A1: (n + 1) mod p = ((n mod p) + 1) mod p by NAT_D:22;

per cases ( k = 0 or k > 0 ) ;

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

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

end;

suppose k > 0 ; :: thesis: (((n mod p) + 1) choose k) mod p = (((n + 1) mod p) choose k) mod p

then reconsider k = k as non zero Nat ;
(n mod p) + 1 <= p by NAT_D:1, INT_1:7;

per cases then ( (n mod p) + 1 = p or (n mod p) + 1 < p ) by XXREAL_0:1;

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

(((n mod p) + 1) choose k) mod p = (0 choose k) mod p by C1, A0, PCK;
hence (((n mod p) + 1) choose k) mod p = (((n + 1) mod p) choose k) mod p by A1, C1; :: thesis: verum

end;

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

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

end;

end;

end;

end;