proposition: Lemma size_odd_poly_eq p : ~~ odd (size p) -> size (odd_poly p) = (size p)./2.
proof: Proof. have [->|p_neq0] := eqVneq p 0; first by rewrite odd_polyC size_poly0. move=> p_odd; rewrite size_poly_eq// -subn1 doubleB subn2 even_halfK//. rewrite prednK ?lead_coef_eq0// ltn_predRL. by move: p_neq0 p_odd; rewrite -size_poly_eq0; case: (size p) => [|[]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)