proposition: Lemma charf_n_separable K x n : [char L].-nat n -> 1 < n -> separable_element K x = (x \in <<K; x ^+ n>>%VS).
proof: Proof. rewrite -pi_pdiv; set p := pdiv n => charLn pi_n_p. have charLp: p \in [char L] := pnatPpi charLn pi_n_p. have <-: (n`_p)%N = n by rewrite -(eq_partn n (charf_eq charLp)) part_pnat_id. by rewrite p_part lognE -mem_primes pi_n_p -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)