proposition: Lemma adjoin_separable : separable_element <<K; y>> x -> separable_element K x.
proof: Proof. have /Derivation_separableP derKy := sepKy => /Derivation_separableP derKy_x. have [z defKz] := Primitive_Element_Theorem. suffices /adjoin_separableP: separable_element K z. by apply; rewrite -defKz memv_adjoin. apply/Derivation_separableP=> D; rewrite -defKz => derKxyD DK_0. suffices derKyD: Derivation <<K; y>>%VS D by rewrite derKy_x // derKy. by apply: DerivationS derKxyD; apply: subv_adjoin. 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)