proposition: Lemma split_sum_even_odd_alt (F: fterm) n: natp n -> csumb (Nint n) F = csumb (Nint (chalf (csucc n))) (fun k => F (cdouble k)) +c csumb (Nint (chalf n)) (fun k => F (csucc (cdouble k))).
proof: Proof. move => nN. case: (equal_or_not n \0c) => nz. rewrite nz succ_zero half0 half1 Nint_co00. rewrite /csumb !csum_trivial; aw; trivial;rewrite csum0r; fprops. case: (equal_or_not n \1c) => no. rewrite no succ_one half1 half2 Nint_co00 /csumb (proj2 Nint_co01). set F1 := Lg _ _; set F2 := Lg _ _. have ha: (domain F1 = singleton \0c) by rewrite /F1; aw. have hb: (domain F2 = singleton \0c) by rewrite /F2; aw. have hc:= (set1_1 \0c). rewrite (csum_trivial1 ha) (csum_trivial1 hb) /F1 /F2 !LgV//. rewrite cdouble0 csum_trivial; aw; trivial; rewrite csum0r; fprops. move: (cpred_pr nN nz) => [sa sb]. have h: (cpred n) <> \0c by move => h; case no; rewrite sb h succ_zero. move:(cpred_pr sa h) => [sa' sb']. move:(split_sum_even_odd F sa h). rewrite (Nint_co_cc sa)(Nint_co_cc ((NS_half sa'))). rewrite (Nint_co_cc (NS_half sa)) -(half_succ sa) -(half_succ sa'). by rewrite - sb' - sb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)