proposition: Lemma subfxE x: exists p, x = subfx_eval p.
proof: Proof. elim/quotW: x => x; exists (rVpoly x); apply/eqP; rewrite piE /equiv_subfext. by rewrite /iotaFz poly_rV_modp_K iotaPz_modp. 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)