proposition: Lemma make_separable p : p != 0 -> separable (p %/ gcdp p p^`()).
proof: Proof. set g := gcdp p p^`() => nz_p; apply/separable_polyP. have max_dvd_u (u : {poly R}): 1 < size u -> exists k, ~~ (u ^+ k %| p). move=> u_gt1; exists (size p); rewrite gtNdvdp // polySpred //. by rewrite -(ltn_subRL 1) subn1 size_exp leq_pmull // -(subnKC u_gt1). split=> [|u u_pg u_gt1]; last first. apply/eqP=> u'0 /=; have [k /negP[]] := max_dvd_u u u_gt1. elim: k => [|k IHk]; first by rewrite dvd1p. suffices: u ^+ k.+1 %| (p %/ g) * g. by rewrite Pdiv.Idomain.divpK ?dvdp_gcdl // dvdpZr ?lcn_neq0. rewrite exprS dvdp_mul // dvdp_gcd IHk //=. suffices: u ^+ k %| (p %/ u ^+ k * u ^+ k)^`(). by rewrite Pdiv.Idomain.divpK // derivZ dvdpZr ?lcn_neq0. by rewrite !derivCE u'0 mul0r mul0rn mulr0 addr0 dvdp_mull. have pg_dv_p: p %/ g %| p by rewrite divp_dvd ?dvdp_gcdl. apply/poly_square_freeP=> u; rewrite neq_ltn ltnS leqn0 size_poly_eq0. case/predU1P=> [-> | /max_dvd_u[k]]. by apply: contra nz_p; rewrite expr0n -dvd0p => /dvdp_trans->. apply: contra => u2_dv_pg; case: k; [by rewrite dvd1p | elim=> [|n IHn]]. exact: dvdp_trans (dvdp_mulr _ _) (dvdp_trans u2_dv_pg pg_dv_p). suff: u ^+ n.+2 %| (p %/ g) * g. by rewrite Pdiv.Idomain.divpK ?dvdp_gcdl // dvdpZr ?lcn_neq0. rewrite -add2n exprD dvdp_mul // dvdp_gcd. rewrite (dvdp_trans _ IHn) ?exprS ?dvdp_mull //=. suff: u ^+ n %| ((p %/ u ^+ n.+1) * u ^+ n.+1)^`(). by rewrite Pdiv.Idomain.divpK // derivZ dvdpZr ?lcn_neq0. by rewrite !derivCE dvdp_add // -1?mulr_natl ?exprS !dvdp_mull. 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)