proposition: Lemma polyOver_subvs {K} {p : {poly L}} : reflect (exists q : {poly subvs_of K}, p = map_poly vsval q) (p \is a polyOver K).
proof: Proof. apply: (iffP polyOverP) => [Hp | [q ->] i]; last by rewrite coef_map // subvsP. exists (\poly_(i < size p) (Subvs (Hp i))); rewrite -{1}[p]coefK. by apply/polyP=> i; rewrite coef_map !coef_poly; case: ifP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)