proposition: Lemma strong_Primitive_Element_Theorem K x y : separable_element <<K; x>> y -> exists2 z : L, (<< <<K; y>>; x>> = <<K; z>>)%VS & separable_element K x -> separable_element K y.
proof: Proof. move=> sepKx_y; have [n /andP[charLn sepKyn]] := separable_exponent K y. have adjK_C z t: (<<<<K; z>>; t>> = <<<<K; t>>; z>>)%VS. by rewrite !agenv_add_id -!addvA (addvC <[_]>%VS). have [z defKz] := Primitive_Element_Theorem x sepKyn. exists z => [|/adjoin_separable->]; rewrite ?sepKx_y // -defKz. have [|n_gt1|-> //] := ltngtP n 1; first by case: (n) charLn. apply/eqP; rewrite !(adjK_C _ x) eqEsubv; apply/andP. split; apply/FadjoinP/andP; rewrite subv_adjoin ?rpredX ?memv_adjoin //=. by rewrite -charf_n_separable ?sepKx_y. 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)