proposition: Lemma separable_root_der : separable_element K x (+) root (minPoly K x)^`() x.
proof: Proof. have KpKx': _^`() \is a polyOver K := polyOver_deriv (minPolyOver K x). rewrite separable_nz_der addNb (root_small_adjoin_poly KpKx') ?addbb //. by rewrite (leq_trans (size_poly _ _)) ?size_minPoly. 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)