proposition: Lemma Fadjoin_idP {K x} : reflect (<<K; x>>%VS = K) (x \in K).
proof: Proof. apply: (iffP idP) => [/addv_idPl-> | <-]; first exact: subfield_closed. exact: memv_adjoin. 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)