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. by case:(odd_dichot n) => ->; rewrite (half_bit_double n./2 true) -? doubleS doubleK ? big_ord_recr split_sum_even_odd1 // addnAC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)