proposition: Lemma split_sum_even_odd (F: nat -> nat) n: \sum_(i<n) (F i) = \sum_(i< (n.+1)./2) (F i.*2) + \sum_(i< n./2) (F i.*2.+1).
proof: Proof. have H k: \sum_(i<k.*2) (F i) = \sum_(i< k) (F i.*2) + \sum_(i< k) (F i.*2.+1). elim:k; first by rewrite !big_ord0. by move => k Hr; rewrite doubleS !big_ord_recr /= Hr addnACA addnA. have: n = (n./2).*2.+1 \/ n = (n./2).*2. by rewrite -{1 3} (odd_double_half n);case: (odd n); [left | right]. by case => ->; rewrite (half_bit_double n./2 true) -? doubleS doubleK ? big_ord_recr H // addnAC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)