proposition: Lemma split_sum_even_odd (F: fterm) n: natp n -> n <> \0c -> csumb (Nintc n) F = csumb (Nintc (chalf n)) (fun k => F (cdouble k)) +c csumb (Nintc (chalf (cpred n))) (fun k => F (csucc (cdouble k))).
proof: Proof. move => nN nz. set A := Zo (Nintc n) evenp. set B := Zo (Nintc n) oddp. have pa: disjoint A B by apply:disjoint_pr => u /Zo_hi eu /Zo_hi [_]. have -> : Nintc n = A \cup B. set_extens t; last by move/setU2_P; case => /Zo_S. case:(p_or_not_p (evenp t)) => et ta; first by apply: setU2_1; apply:Zo_i. apply: setU2_2; apply:Zo_i => //; split => //; apply: (Nint_S ta). move:(NS_half nN) => hN. move: (cpred_pr nN nz) => [pN pv]. move:(NS_half pN) => hpN. rewrite (csumA_setU2 _ pa); apply: f_equal2;apply:csum_Cn2; split. + move => x /(NintcP hN) xle; move:(NS_le_nat xle hN) => xN. apply/Zo_P; split; last by apply:even_double. by apply/(NintcP nN); apply:half_monotone2. + by move => x y /Nint_S xN /Nint_S yN; move/(double_inj xN yN). + move => y /Zo_P[yi ye]; move:(half_even ye) => he; exists (chalf y) => //. by apply /(NintcP hN); move/(NintcP nN): yi => /(half_monotone (proj1 ye) nN). + move => x /(NintcP hpN) xle; move:(NS_le_nat xle hpN) => xN. apply/Zo_P; split; last by apply:odd_succ_double. apply/(NintcP nN); rewrite pv. by apply/(cleSSP (CS_nat (NS_double xN)) (CS_nat pN));apply: half_monotone2. + move => x y /Nint_S xN /Nint_S yN. have ha: (cardinalp (cdouble x)) by rewrite /cdouble; fprops. have hb: (cardinalp (cdouble y)) by rewrite /cdouble; fprops. by move/ (csucc_inj ha hb) /(double_inj xN yN). + move => y /Zo_P[yi yo]; move:(half_odd yo) => he; exists (chalf y) => //. apply /(NintcP hpN); move/(NintcP nN): yi. have ha: (cardinalp (cdouble(chalf y))) by rewrite /cdouble; fprops. have hb: cardinalp (cdouble (chalf (cpred n))) by rewrite /cdouble; fprops. have hyN := (NS_half (proj1 yo)). have hc: cardinalp (csucc (cdouble (chalf (cpred n)))) by apply: CS_succ. rewrite {1} pv {1} he;case: (cdouble_halfV pN) => eq; rewrite {1} eq. move/(cleSSP ha hb) => h. by apply/(double_monotone hyN hpN). have hf:natp (csucc (cdouble (chalf (cpred n)))) by rewrite -eq. move/(cleSSP ha hc); move/(cltSleP hf); rewrite - (double_succ hpN). by move/(double_monotone2 hyN (NS_succ hpN))/(cltSleP hpN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)