proposition: Lemma FadjoinP {K x E} : reflect (K <= E /\ x \in E)%VS (<<K; x>>%AS <= E)%VS.
proof: Proof. apply: (iffP idP) => [sKxE | /andP]. by rewrite (subvP sKxE) ?memv_adjoin // (subv_trans _ sKxE) ?subv_adjoin. by rewrite -subv_add => /agenvS; rewrite subfield_closed. 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)