proposition: Lemma Fadjoin_seqP {K} {rs : seq L} {E} : reflect (K <= E /\ {subset rs <= E})%VS (<<K & rs>> <= E)%VS.
proof: Proof. apply: (iffP idP) => [sKrsE | [sKE /span_subvP/(conj sKE)/andP]]. split=> [|x rs_x]; first exact: subv_trans (subv_adjoin_seq _ _) sKrsE. by rewrite (subvP sKrsE) ?seqv_sub_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)