proposition: Lemma Fadjoin_polyP {v} : reflect (exists2 p, p \in polyOver K & v = p.[x]) (v \in <<K; x>>%VS).
proof: Proof. apply: (iffP idP) => [Kx_v | [p Kp ->]]; last exact: mempx_Fadjoin. by exists (Fadjoin_poly K x v); rewrite ?Fadjoin_polyOver ?Fadjoin_poly_eq. 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)