proposition: Lemma size_even_poly_eq p : odd (size p) -> size (even_poly p) = uphalf (size p).
proof: Proof. move=> p_even; rewrite size_poly_eq// double_pred odd_uphalfK//=. by rewrite lead_coef_eq0 -size_poly_eq0; case: size p_even. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)