proposition: Lemma even_polyE s p : size p <= s.*2 -> even_poly p = \poly_(i < s) p`_i.*2.
proof: Proof. move=> pLs2; apply/polyP => i; rewrite coef_even_poly !coef_poly if_nth //. by case: ltnP => //= ?; rewrite (leq_trans pLs2) ?leq_double. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)