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