proposition: Lemma purely_inseparable_elementP {K x} : reflect (exists2 n, [char L].-nat n & x ^+ n \in K) (purely_inseparable_element K x).
proof: Proof. rewrite /purely_inseparable_element. case: ex_minnP => n /andP[charLn /=]; rewrite subfield_closed => sepKxn min_xn. apply: (iffP idP) => [Kxn | [m charLm Kxm]]; first by exists n. have{min_xn}: n <= m by rewrite min_xn ?charLm ?base_separable. rewrite leq_eqVlt => /predU1P[-> // | ltnm]; pose p := pdiv m. have m_gt1: 1 < m by have [/leq_ltn_trans->] := andP charLn. have charLp: p \in [char L] by rewrite (pnatPpi charLm) ?pi_pdiv. have [/p_natP[em Dm] /p_natP[en Dn]]: p.-nat m /\ p.-nat n. by rewrite -!(eq_pnat _ (charf_eq charLp)). rewrite Dn Dm ltn_exp2l ?prime_gt1 ?pdiv_prime // in ltnm. rewrite -(Fadjoin_idP Kxm) Dm -(subnKC ltnm) addSnnS expnD exprM -Dn. by rewrite -charf_p_separable. 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)