proposition: Lemma Derivation_separableP : reflect (forall D, Derivation <<K; x>> D -> K <= lker D -> <<K; x>> <= lker D)%VS (separable_element K x).
proof: Proof. apply: (iffP idP) => [sepKx D derD /subvP DK_0 | derKx_0]. have{} DK_0 q: q \is a polyOver K -> map_poly D q = 0. move=> /polyOverP Kq; apply/polyP=> i; apply/eqP. by rewrite coef0 coef_map -memv_ker DK_0. apply/subvP=> _ /Fadjoin_polyP[p Kp ->]; rewrite memv_ker. rewrite (Derivation_horner derD) ?(polyOverSv sKxK) //. rewrite (Derivation_separable derD sepKx) !DK_0 ?minPolyOver //. by rewrite horner0 oppr0 mul0r mulr0 addr0. apply: wlog_neg; rewrite {1}separable_nz_der negbK => /eqP pKx'_0. pose Df := fun y => (Fadjoin_poly K x y)^`().[x]. have Dlin: linear Df. move=> a u v; rewrite /Df linearP /= -mul_polyC derivD derivM derivC. by rewrite mul0r add0r hornerD hornerM hornerC -scalerAl mul1r. pose DlinM := GRing.isLinear.Build _ _ _ _ Df Dlin. pose DL : GRing.Linear.type _ _ := HB.pack Df DlinM. pose D := linfun DL; apply: base_separable. have DK_0: (K <= lker D)%VS. apply/subvP=> v Kv; rewrite memv_ker lfunE /= /Df Fadjoin_polyC //. by rewrite derivC horner0. have Dder: Derivation <<K; x>> D. apply/allrelP=> u v /vbasis_mem Kx_u /vbasis_mem Kx_v; apply/eqP. rewrite !lfunE /= /Df; set Px := Fadjoin_poly K x. set Px_u := Px u; rewrite -(Fadjoin_poly_eq Kx_u) -/Px -/Px_u. set Px_v := Px v; rewrite -(Fadjoin_poly_eq Kx_v) -/Px -/Px_v. rewrite -!hornerM -hornerD -derivM. rewrite /Px Fadjoin_poly_mod ?rpredM ?Fadjoin_polyOver //. rewrite [in RHS](divp_eq (Px_u * Px_v) (minPoly K x)) derivD derivM. by rewrite pKx'_0 mulr0 addr0 hornerD hornerM minPolyxx mulr0 add0r. have{Dder DK_0}: x \in lker D by apply: subvP Kx_x; apply: derKx_0. apply: contraLR => K'x; rewrite memv_ker lfunE /= /Df Fadjoin_polyX //. by rewrite derivX hornerC oner_eq0. 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)