proposition: Lemma Fadjoin1_polyP x v : reflect (exists p, v = (map_poly (in_alg L) p).[x]) (v \in <<1; x>>%VS).
proof: Proof. apply: (iffP Fadjoin_polyP) => [[_ /polyOver1P]|] [p ->]; first by exists p. by exists (map_poly (in_alg L) p) => //; apply: alg_polyOver. 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)