proposition: Lemma separable_inseparable_decomposition E K : {x | x \in E /\ separable_element K x & purely_inseparable <<K; x>> E}.
proof: Proof. without loss sKE: K / (K <= E)%VS. case/(_ _ (capvSr K E)) => x [Ex sepKEx] /purely_inseparableP sep'KExE. exists x; first by split; last exact/(separable_elementS _ sepKEx)/capvSl. apply/purely_inseparableP=> y /sep'KExE; apply: sub_inseparable. exact/adjoinSl/capvSl. pose E_ i := (vbasis E)`_i; pose fP i := separable_exponent K (E_ i). pose f i := E_ i ^+ ex_minn (fP i); pose s := mkseq f (\dim E). pose K' := <<K & s>>%VS. have sepKs: all (separable_element K) s. by rewrite all_map /f; apply/allP=> i _ /=; case: ex_minnP => m /andP[]. have [x sepKx defKx]: {x | x \in E /\ separable_element K x & K' = <<K; x>>%VS}. have: all [in E] s. rewrite all_map; apply/allP=> i; rewrite mem_iota => ltis /=. by rewrite rpredX // vbasis_mem // memt_nth. rewrite {}/K'; elim/last_ind: s sepKs => [|s t IHs]. by exists 0; [rewrite base_separable mem0v | rewrite adjoin_nil addv0]. rewrite adjoin_rcons !all_rcons => /andP[sepKt sepKs] /andP[/= Et Es]. have{IHs sepKs Es} [y [Ey sepKy] ->{s}] := IHs sepKs Es. have /sig_eqW[x defKx] := Primitive_Element_Theorem t sepKy. exists x; [split | exact: defKx]. suffices: (<<K; x>> <= E)%VS by case/FadjoinP. by rewrite -defKx !(sameP FadjoinP andP) sKE Ey Et. apply/adjoin_separableP=> z; rewrite -defKx => Kyt_z. apply: adjoin_separable sepKy _; apply: adjoin_separableP Kyt_z. exact: separable_elementS (subv_adjoin K y) sepKt. exists x; rewrite // -defKx; apply/(all_nthP 0)=> i; rewrite size_tuple => ltiE. apply/purely_inseparable_elementP. exists (ex_minn (fP i)); first by case: ex_minnP => n /andP[]. by apply/seqv_sub_adjoin/map_f; rewrite mem_iota. 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)