proposition: Lemma eq_adjoin_separable_generator E K : separable K E -> (K <= E)%VS -> E = <<K; separable_generator K E>>%VS :> {vspace _}.
proof: Proof. move=> sepK_E sKE; apply/eqP; rewrite eqEsubv sub_adjoin_separable_generator //. by apply/FadjoinP/andP; rewrite sKE separable_generator_mem. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset prime) mathcomp(binomial ssralg poly polydiv fingroup perm) mathcomp(morphism quotient gproduct finalg zmodp cyclic) mathcomp(matrix mxalgebra mxpoly polyXY vector falgebra) mathcomp(fieldext)