proposition: Lemma subfxEroot x : {q | x = (map_poly (in_alg subFExtend) q).[subfx_root]}.
proof: Proof. have /sig_eqW[q ->] := subfxE x; exists q. apply: (fmorph_inj subfx_inj). rewrite -horner_map /= subfx_inj_root subfx_inj_eval //. by rewrite -map_poly_comp (eq_map_poly subfx_inj_base). 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)