proposition: Lemma odd_polyMX p : odd_poly (p * 'X) = even_poly p.
proof: Proof. have [->|pN0] := eqVneq p 0; first by rewrite mul0r even_polyC odd_polyC. by apply/polyP => i; rewrite !coef_poly size_mulX // coefMX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)