proposition: Lemma bin_mod2_prop3 n k: natp n -> natp k -> eqmod \2c (binom (csucc (cdouble n)) (csucc (cdouble k))) (binom n k).
proof: Proof. move => nN kN. move:(NS_double nN)(NS_double kN) => n2N k2N. move: (NS_binom n2N (NS_succ k2N)) (NS_binom n2N k2N) => ha hb. have he := (NS_binom nN kN). rewrite (binomSnSm n2N k2N) /eqmod (crem_sum NS2 card2_nz ha hb). rewrite (bin_mod2_rec2 nN kN) (bin_mod2_prop1 nN kN). by rewrite (Nsum0l (NS_rem \2c he)) (cmodmod2 he). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)