proposition: Lemma sum_diag_pascal_prop n: natp n -> (sum_diag_pascal2 n) = fusc (csucc n).
proof: Proof. move: n. suff: forall n, natp n -> n <> \0c -> (sum_diag_pascal2 (cpred n)) = fusc n. move => H n nN. rewrite - {1} (cpred_pr2 nN); apply:(H _ (NS_succ nN) (@succ_nz _)). apply: fusc_induction. + done. + move => _. rewrite - {1} succ_zero (cpred_pr2 NS0) fusc1;apply:sum_diag_pascal2_0. + move => n nN H dnz; case: (equal_or_not n \0c) => enz. by case: dnz; rewrite enz cdouble0. move:(cpred_pr nN enz) => [sa sb]; rewrite (fusc_even nN) - (H enz). rewrite {1} sb (double_succ sa) (cpred_pr2 (NS_succ (NS_double sa))). rewrite (sum_diag_pascal_mod2_odd sa) //; apply: NS_succ. + move => k kN H1 H2 _. rewrite (fusc_odd kN) (cpred_pr2 (NS_double kN)). case: (equal_or_not k \0c) => ekn. by rewrite ekn cdouble0 succ_zero fusc0 fusc1 sum_diag_pascal2_0(csum0l CS1). move:(cpred_pr kN ekn) => [sa sb]. rewrite sb (double_succ sa) (sum_diag_pascal_mod2_even sa). by rewrite - sb (H1 ekn) csumC - (H2 (@succ_nz _)) (cpred_pr2 kN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)