proposition: Lemma poly_even_odd p : even_poly p \Po 'X^2 + (odd_poly p \Po 'X^2) * 'X = p.
proof: Proof. rewrite -sum_even_poly -sum_odd_poly addrC -(bigID _ xpredT). by rewrite -[RHS]coefK poly_def. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)