proposition: Lemma separable_exponent K x : exists n, [char L].-nat n && separable_element K (x ^+ n).
proof: Proof. pose d := adjoin_degree K x; move: {2}d.+1 (ltnSn d) => n. elim: n => // n IHn in x @d *; rewrite ltnS => le_d_n. have [[p charLp]|] := altP (separablePn K x); last by rewrite negbK; exists 1. case=> g Kg defKx; have p_pr := charf_prime charLp. suffices /IHn[m /andP[charLm sepKxpm]]: adjoin_degree K (x ^+ p) < n. by exists (p * m)%N; rewrite pnatM pnatE // charLp charLm exprM. apply: leq_trans le_d_n; rewrite -ltnS -!size_minPoly. have nzKx: minPoly K x != 0 by rewrite monic_neq0 ?monic_minPoly. have nzg: g != 0 by apply: contra_eqN defKx => /eqP->; rewrite comp_poly0. apply: leq_ltn_trans (dvdp_leq nzg _) _. by rewrite minPoly_dvdp // rootE -hornerXn -horner_comp -defKx minPolyxx. rewrite (polySpred nzKx) ltnS defKx size_comp_poly size_polyXn /=. suffices g_gt1: 1 < size g by rewrite -(subnKC g_gt1) ltn_Pmulr ?prime_gt1. apply: contra_eqT (size_minPoly K x); rewrite defKx -leqNgt => /size1_polyC->. by rewrite comp_polyC size_polyC; case: (_ != 0). 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)