proposition: Lemma bin_mod2_prop2 n k: natp n -> natp k -> eqmod \2c (binom (csucc (cdouble n)) (cdouble k)) (binom n k).
proof: Proof. move => nN kN. case: (equal_or_not k \0c) => ekz. rewrite ekz cdouble0 !binom0 //; fprops; apply:(NS_succ(NS_double nN)). move:(cpred_pr kN ekz) => [sa ->]. have ha:=(NS_double nN). have hb:=(NS_succ(NS_double sa)). have hc:= (NS_binom ha (NS_double (NS_succ sa))). have he:=(NS_binom nN (NS_succ sa)). have hd:=(NS_binom ha hb). rewrite (double_succ sa) (binomSnSm ha hb) /eqmod - (double_succ sa). rewrite (crem_sum NS2 card2_nz hc hd) (bin_mod2_rec2 nN (NS_succ sa)). by rewrite (bin_mod2_prop1 nN sa) (Nsum0r (NS_rem \2c he)) (cmodmod2 he). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)