proposition: Lemma char0_minPoly_separable x E : separable_poly (minPoly E x).
proof: Proof. have pE := minPolyOver E x; set p := minPoly E x. suff /eqp_separable-> : p %= p %/ gcdp p p^`(). by rewrite make_separable ?monic_neq0 ?monic_minPoly. rewrite /eqp divp_dvd ?dvdp_gcdl// andbT. rewrite minPoly_dvdp ?divp_polyOver ?gcdp_polyOver ?polyOver_deriv//. by rewrite -root_make_separable// root_minPoly. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra all_field)