proposition: Lemma sum_diag_pascal_mod2_odd n (S := sum_diag_pascal2) : natp n -> S (csucc (cdouble n)) = S n.
proof: Proof. move => nN. have dN := (NS_double nN). have h:=(NS_succ dN). rewrite /S /sum_diag_pascal2 (split_sum_even_odd _ h (@succ_nz _)). rewrite (odd_half nN) (cpred_pr2 dN) (even_half nN). set A := ( X in X +c _ ); set B := csumb _ _. have cA: cardinalp A by apply:CS_csum. have ->: B = csumb (Nintc n) (fun i => \0c). rewrite /B/cst_graph /csumb; apply:f_equal; apply:Lg_exten. move => i /(NintcP nN) lein; move:(NS_le_nat lein nN) => iN. rewrite (cdiff_pr6 dN (NS_double iN)). by rewrite - (cprodBl NS2 nN iN) (bin_mod2_prop1 (NS_diff i nN) iN). rewrite csum_of_same cprod0l (csum0r cA) /A /csumb. apply:f_equal; apply:Lg_exten => i ii; move:(Nint_S ii) => iN. move /(NintcP nN): ii => /(double_monotone iN nN) /(cdiffSn dN) ->. rewrite - (cprodBl NS2 nN iN);apply: (bin_mod2_prop2 (NS_diff i nN) iN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)