proposition: Lemma sum_of_i3 n: natp n -> csumb n id = binom n \2c.
proof: Proof. move=> nN. move: clt_02 => lt20. case: (equal_or_not n \0c) => nz. by rewrite nz (binom_bad NS0 NS2 clt_02) csum_trivial0. move: (cpred_pr nN nz); set p := cpred n; move => [pN nsp]. rewrite nsp (binom2 pN). set sn:= csumb n id; set aux:= (p *c (csucc p)). suff eq: (sn +c sn = aux). move:(NS_prod pN (NS_succ pN)); rewrite - /aux - eq => aN. have qN: natp sn by apply: NS_in_sumr aN; rewrite /sn/csumb; fprops. by rewrite csum_nn -nsp [RHS] even_half. rewrite /aux cprodC /sn nsp. rewrite nsp in nN. have fim: (forall i, i <c (csucc p) -> (fun i=> i +c (p -c i)) i = p). by move=> i /(cltSleP pN) => ilp; apply: cdiff_pr. rewrite - (fct_sum_const1 nN fim). rewrite - (sum_of_sums (fun i => i) (fun i=> (p -c i)) (csucc p)). apply: f_equal. by apply: fct_sum_rev. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)