proposition: Lemma separable_nz_der : separable_element K x = ((minPoly K x)^`() != 0).
proof: Proof. rewrite /separable_element unlock. apply/idP/idP=> [|nzPx']. by apply: contraTneq => ->; rewrite coprimep0 -size_poly_eq1 size_minPoly. have gcdK : gcdp (minPoly K x) (minPoly K x)^`() \in polyOver K. by rewrite gcdp_polyOver ?polyOver_deriv // minPolyOver. rewrite -gcdp_eqp1 -size_poly_eq1 -dvdp1. have /orP[/andP[_]|/andP[]//] := minPoly_irr gcdK (dvdp_gcdl _ _). rewrite dvdp_gcd dvdpp /= => /(dvdp_leq nzPx')/leq_trans/(_ (size_poly _ _)). by rewrite size_minPoly ltnn. 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)