proposition: Lemma sum_diag_pascal_mod2_even n (S := sum_diag_pascal2) : natp n -> S (csucc (csucc (cdouble n))) = S (csucc n) +c S n.
proof: Proof. move => nN. have ha:= (NS_succ nN); have dnN := (NS_double nN). have hb:= (NS_succ dnN); have hc:=(NS_succ hb). rewrite /S /sum_diag_pascal2 (split_sum_even_odd _ hc (@succ_nz _)). rewrite (cpred_pr2 hb) (odd_half nN). rewrite - (double_succ nN) (even_half ha); apply: f_equal2; rewrite/csumb; apply: f_equal; apply: Lg_exten => i ii;move:(Nint_S ii) => iN. + rewrite - (cprodBl NS2 ha iN); apply:(bin_mod2_rec2 (NS_diff i ha) iN). + rewrite (double_succ nN) (cdiff_pr6 hb (NS_double iN)). move /(NintcP nN): ii => /(double_monotone iN nN) /(cdiffSn dnN) ->. rewrite - (cprodBl NS2 nN iN); apply:(bin_mod2_prop3 (NS_diff i nN) iN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)