proposition: Lemma sum_odd_poly p : \sum_(i < size p | odd i) p`_i *: 'X^i = (odd_poly p \Po 'X^2) * 'X.
proof: Proof. apply/polyP => i; rewrite coefMX coef_comp_poly_Xn// coef_sumMXn coef_odd_poly/=. case: i => [|i]//=; first by rewrite big_andbC big1// => -[[|j]//]. rewrite big_ord1_cond_eq/= -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)