proposition: Lemma separable_polyP {p} : reflect [/\ forall u v, u * v %| p -> coprimep u v & forall u, u %| p -> 1 < size u -> u^`() != 0] (separable p).
proof: Proof. apply: (iffP idP) => [sep_p | [sq'p nz_der1p]]. split=> [u v | u u_dv_p]; last first. apply: contraTneq => u'0; rewrite unlock in sep_p; rewrite -leqNgt -(eqnP sep_p). rewrite dvdp_leq -?size_poly_eq0 ?(eqnP sep_p) // dvdp_gcd u_dv_p. have /dvdpZr <-: lead_coef u ^+ scalp p u != 0 by rewrite lcn_neq0. by rewrite -derivZ -Pdiv.Idomain.divpK //= derivM u'0 mulr0 addr0 dvdp_mull. rewrite Pdiv.Idomain.dvdp_eq mulrCA mulrA; set c := _ ^+ _ => /eqP Dcp. have nz_c: c != 0 by rewrite lcn_neq0. move: sep_p; rewrite coprimep_sym unlock -(coprimepZl _ _ nz_c). rewrite -(coprimepZr _ _ nz_c) -derivZ Dcp derivM coprimepMl. by rewrite coprimep_addl_mul !coprimepMr -andbA => /and4P[]. rewrite unlock coprimep_def eqn_leq size_poly_gt0; set g := gcdp _ _. have nz_g: g != 0. rewrite -dvd0p dvdp_gcd -(mulr0 0); apply/nandP; left. by have /poly_square_freeP-> := sq'p; rewrite ?size_poly0. have [g_p]: g %| p /\ g %| p^`() by rewrite dvdp_gcdr ?dvdp_gcdl. pose c := lead_coef g ^+ scalp p g; have nz_c: c != 0 by rewrite lcn_neq0. have Dcp: c *: p = p %/ g * g by rewrite Pdiv.Idomain.divpK. rewrite nz_g andbT leqNgt -(dvdpZr _ _ nz_c) -derivZ Dcp derivM. rewrite dvdp_addr; last by rewrite dvdp_mull. rewrite Gauss_dvdpr; last by rewrite sq'p // mulrC -Dcp dvdpZl. by apply: contraL => /nz_der1p nz_g'; rewrite gtNdvdp ?nz_g' ?lt_size_deriv. 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)