proposition: Lemma bin_mod2_rec1 n k : natp n -> natp k -> eqmod \2c (binom (csucc (csucc n)) (csucc (csucc k))) ((binom n (csucc (csucc k))) +c (binom n k)).
proof: Proof. move => nN kN. move: (NS_succ nN) (NS_succ kN) => snN skN. rewrite (binomSnSm snN skN) (binomSnSm nN skN) (binomSnSm nN kN). set A := binom _ _;rewrite csumA - (csumA A) (csumC A) csum_nn - csumA. apply:(crem_prop NS2 card2_nz); try apply: NS_sum;apply: NS_binom; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)