proposition: Lemma sum_even_poly p : \sum_(i < size p | ~~ odd i) p`_i *: 'X^i = even_poly p \Po 'X^2.
proof: Proof. apply/polyP => i; rewrite coef_comp_poly_Xn// coef_sumMXn coef_even_poly. rewrite (big_ord1_cond_eq _ _ (negb \o _))/= -dvdn2 andbC -muln2. by case: dvdnP => //= -[k ->]; rewrite mulnK// if_nth ?leqVgt. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)