proposition: Lemma split_sum_even_odd1 (F: nat -> nat) n: \sum_(i<n.*2) (F i) = \sum_(i< n) (F i.*2) + \sum_(i< n) (F i.*2.+1).
proof: Proof. elim:n; first by rewrite !big_ord0. by move => k Hr; rewrite doubleS !big_ord_recr /= Hr addnACA addnA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)