proposition: Lemma bin_mod2_rec2 n k: natp n -> natp k -> eqmod \2c (binom (cdouble n) (cdouble k)) (binom n k).
proof: Proof. move => nN kN; case: (equal_or_not k \0c) => knz. by rewrite knz cdouble0 ! binom0 //; apply: NS_double. move: (cpred_pr kN knz) => [sa ->]. move: {k kN knz} n nN (cpred k) sa; apply: Nat_induction. move => k kN. have ha: \0c <c csucc k by apply: succ_positive. have hb: \0c <c (cdouble (csucc k)). by rewrite (double_succ kN); apply: succ_positive. rewrite cdouble0 (binom_bad NS0 (NS_double (NS_succ kN)) hb). by rewrite (binom_bad NS0 (NS_succ kN) ha). move => n nN Hrec k kN. have dnN := NS_double nN. have dkN := NS_double kN. have dskN := NS_double (NS_succ kN). have ha: natp (binom (cdouble n) (cdouble (csucc k))) by apply:NS_binom;fprops. have hb: natp (binom (cdouble n) (cdouble k)) by apply:NS_binom;fprops. have hc:=(NS_binom nN (NS_succ kN)); have hd:= (NS_binom nN kN). rewrite (double_succ nN) (double_succ kN). rewrite /eqmod (bin_mod2_rec1 (NS_double nN) (NS_double kN)). rewrite - (double_succ kN) (crem_sum NS2 card2_nz ha hb) (Hrec _ kN). rewrite (binomSnSm nN kN) (crem_sum NS2 card2_nz hc hd). congr ((_ +c _) %%c \2c); case: (equal_or_not k \0c) => ekz. rewrite ekz cdouble0 !binom0 //. by move:(cpred_pr kN ekz) => [pN ->]; apply:Hrec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)