proposition: Lemma bin_mod2_prop1 n k: natp n -> natp k -> (binom (cdouble n) (csucc (cdouble k))) %%c \2c = \0c.
proof: Proof. move => nN kN. case: (equal_or_not k \0c) => ekz. rewrite ekz cdouble0 succ_zero (binom1 (NS_double nN)). apply:(proj33(cdivides_pr1 nN NS2)). move: (cpred_pr kN ekz) => [sa ->]. move: {k kN ekz} n nN (cpred k) sa; apply: Nat_induction. move => k kN. have ha: \0c <c csucc (cdouble (csucc k)) by apply: succ_positive. have hb:= (NS_succ (NS_double (NS_succ kN))). by rewrite cdouble0 (binom_bad NS0 hb ha) (crem_of_zero NS2). move => n nN Hrec k kN. have dnN := NS_double nN. have dkN := NS_double kN. have sdkN := NS_succ dkN. have sdskN := NS_succ (NS_double (NS_succ kN)). have ha:natp (binom (cdouble n) (csucc (cdouble (csucc k)))) by apply:NS_binom. have hb:natp (binom (cdouble n) (csucc (cdouble k))) by apply:NS_binom. rewrite (double_succ nN) (double_succ kN) /eqmod (bin_mod2_rec1 dnN sdkN). rewrite -(double_succ kN) (crem_sum NS2 card2_nz ha hb). have ->: binom (cdouble n) (csucc (cdouble k)) %%c \2c = \0c. case: (equal_or_not k \0c) => knz. rewrite knz cdouble0 succ_zero (binom1 dnN). exact: (proj33(cdivides_pr1 nN NS2)). by move:(cpred_pr kN knz) => [sa ->]; apply: Hrec. by rewrite (Hrec _ kN) (csum0r CS0) (crem_of_zero NS2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)