Library mathcomp.real_closed.polyrcf

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
From mathcomp
Require Import bigop ssralg poly polydiv ssrnum zmodp.
From mathcomp
Require Import polyorder path interval ssrint.


Import GRing.Theory Num.Theory Num.Def.
Import Pdiv.Idomain.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope nat_scope.
Local Open Scope ring_scope.

Local Notation noroot p := (forall x, ~~ root p x).
Local Notation mid x y := ((x + y) / 2%:R).

Section more.
Section SeqR.

Lemma last1_neq0 (R : ringType) (s : seq R) (c : R) :
  c != 0 -> (last c s != 0) = (last 1 s != 0).
Proof. by elim: s c => [|t s ihs] c cn0 //; rewrite oner_eq0 cn0. Qed.

End SeqR.

Section poly.
Import Pdiv.Ring Pdiv.ComRing.

Variable R : idomainType.

Implicit Types p q : {poly R}.

Lemma lead_coefDr p q :
  (size q > size p)%N -> lead_coef (p + q) = lead_coef q.
Proof. by move/lead_coefDl<-; rewrite addrC. Qed.

Lemma leq1_size_polyC (c : R) : (size c%:P <= 1)%N.
Proof. by rewrite size_polyC; case: (c == 0). Qed.

Lemma my_size_exp p n :
  p != 0 -> (size (p ^+ n)) = ((size p).-1 * n).+1%N.
Proof.
by move=> hp; rewrite -size_exp prednK // lt0n size_poly_eq0 expf_neq0.
Qed.

Lemma coef_comp_poly p q n :
  (p \Po q)`_n = \sum_(i < size p) p`_i * (q ^+ i)`_n.
Proof.
rewrite comp_polyE coef_sum.
by elim/big_ind2: _ => [//|? ? ? ? -> -> //|i]; rewrite coefZ.
Qed.

Lemma gt_size_poly p n : (size p > n)%N -> p != 0.
Proof.
by move=> h; rewrite -size_poly_eq0 lt0n_neq0 //; apply: leq_ltn_trans h.
Qed.

Lemma lead_coef_comp_poly p q :
   (size q > 1)%N ->
  lead_coef (p \Po q) = (lead_coef p) * (lead_coef q) ^+ (size p).-1.
Proof.
move=> sq; rewrite !lead_coefE coef_comp_poly size_comp_poly.
case hp: (size p) => [|n].
  move/eqP: hp; rewrite size_poly_eq0 => /eqP ->.
  by rewrite big_ord0 coef0 mul0r.
rewrite big_ord_recr /= big1 => [|i _].
  by rewrite add0r -lead_coefE -lead_coef_exp lead_coefE size_exp mulnC.
rewrite [X in _ * X]nth_default ?mulr0 ?(leq_trans (size_exp_leq _ _)) //.
by rewrite mulnC ltn_mul2r -subn1 subn_gt0 sq /=.
Qed.

End poly.
End more.

Section PolyNumDomain.

Variable R : numDomainType.
Implicit Types (p q : {poly R}).

Definition sgp_pinfty (p : {poly R}) := sgr (lead_coef p).
Definition sgp_minfty (p : {poly R}) :=
  sgr ((-1) ^+ (size p).-1 * (lead_coef p)).

End PolyNumDomain.

Section PolyRealField.

Variable R : realFieldType.
Implicit Types (p q : {poly R}).

Section SgpInfty.

Lemma sgp_pinfty_sym p : sgp_pinfty (p \Po -'X) = sgp_minfty p.
Proof.
rewrite /sgp_pinfty /sgp_minfty lead_coef_comp_poly ?size_opp ?size_polyX //.
by rewrite lead_coef_opp lead_coefX mulrC.
Qed.

Lemma poly_pinfty_gt_lc p :
   lead_coef p > 0 ->
  exists n, forall x, x >= n -> p.[x] >= lead_coef p.
Proof.
elim/poly_ind: p => [| q c IHq]; first by rewrite lead_coef0 ltrr.
have [->|q_neq0] := eqVneq q 0.
  by rewrite mul0r add0r lead_coefC => c_gt0; exists 0 => x _; rewrite hornerC.
rewrite lead_coefDl ?size_mul ?polyX_eq0 // ?lead_coefMX; last first.
  rewrite size_polyX addn2 size_polyC /= ltnS.
  by rewrite (leq_trans (leq_b1 _)) // size_poly_gt0.
move=> lq_gt0; have [y Hy] := IHq lq_gt0.
pose z := (1 + (lead_coef q) ^-1 * `|c|); exists (maxr y z) => x.
have z_gt0 : 0 < z by rewrite ltr_spaddl ?ltr01 ?mulr_ge0 ?invr_ge0 // ltrW.
rewrite !hornerE ler_maxl => /andP[/Hy Hq Hc].
rewrite (@ler_trans _ (lead_coef q * z + c)) //; last first.
  rewrite ler_add2r (@ler_trans _ (q.[x] * z)) // ?ler_pmul2r //.
  by rewrite ler_pmul2l // (ltr_le_trans _ Hq).
rewrite mulrDr mulr1 -addrA ler_addl mulVKf ?gtr_eqF //.
by rewrite -[c]opprK subr_ge0 normrN ler_norm.
Qed.

Lemma poly_lim_infty p m :
    lead_coef p > 0 -> (size p > 1)%N ->
  exists n, forall x, x >= n -> p.[x] >= m.
Proof.
elim/poly_ind: p m => [| q c _] m; first by rewrite lead_coef0 ltrr.
have [-> _|q_neq0] := eqVneq q 0.
  by rewrite mul0r add0r size_polyC ltnNge leq_b1.
rewrite lead_coefDl ?size_mul ?polyX_eq0 // ?lead_coefMX; last first.
  rewrite size_polyX addn2 size_polyC /= ltnS.
  by rewrite (leq_trans (leq_b1 _)) // size_poly_gt0.
move=> lq_gt0; have [y Hy _] := poly_pinfty_gt_lc lq_gt0.
pose z := (1 + (lead_coef q) ^-1 * (`|m| + `|c|)); exists (maxr y z) => x.
have z_gt0 : 0 < z.
  by rewrite ltr_spaddl ?ltr01 ?mulr_ge0 ?invr_ge0 ?addr_ge0 // ?ltrW.
rewrite !hornerE ler_maxl => /andP[/Hy Hq Hc].
rewrite (@ler_trans _ (lead_coef q * z + c)) //; last first.
  rewrite ler_add2r (@ler_trans _ (q.[x] * z)) // ?ler_pmul2r //.
  by rewrite ler_pmul2l // (ltr_le_trans _ Hq).
rewrite mulrDr mulr1 mulVKf ?gtr_eqF // addrA -addrA ler_paddr //.
  by rewrite -[c]opprK subr_ge0 normrN ler_norm.
by rewrite ler_paddl ?ler_norm // ?ltrW.
Qed.

End SgpInfty.

Section CauchyBound.

Definition cauchy_bound (p : {poly R}) :=
  1 + `|lead_coef p|^-1 * \sum_(i < size p) `|p`_i|.

Lemma cauchy_boundP (p : {poly R}) x :
  p != 0 -> p.[x] = 0 -> `| x | < cauchy_bound p.
Proof.
move=> np0 rpx; rewrite ltr_spaddl ?ltr01 //.
case e: (size p) => [|n]; first by move: np0; rewrite -size_poly_eq0 e eqxx.
have lcp : `|lead_coef p| > 0 by move: np0; rewrite -lead_coef_eq0 -normr_gt0.
have lcn0 : `|lead_coef p| != 0 by rewrite normr_eq0 -normr_gt0.
case: (lerP `|x| 1) => cx1.
  rewrite (ler_trans cx1) // /cauchy_bound ler_pdivl_mull // mulr1.
  by rewrite big_ord_recr /= /lead_coef e ler_addr sumr_ge0.
case es: n e => [|m] e.
  suff p0 : p = 0 by rewrite p0 eqxx in np0.
    by move: rpx; rewrite (@size1_polyC _ p) ?e ?lerr // hornerC; move->.
move: rpx; rewrite horner_coef e -es big_ord_recr /=; move/eqP; rewrite eq_sym.
rewrite -subr_eq sub0r; move/eqP => h1.
have {h1} h1 : `|p`_n| * `|x| ^+ n <= \sum_(i < n) `|p`_i * x ^+ i|.
  rewrite -normrX -normrM -normrN h1.
  by rewrite (ler_trans (ler_norm_sum _ _ _)) // lerr.
have xp : `| x | > 0 by rewrite (ltr_trans _ cx1) ?ltr01.
move: h1; rewrite {-1}es exprS mulrA -ler_pdivl_mulr ?exprn_gt0 //.
rewrite big_distrl /= big_ord_recr /= normrM normrX -mulrA es mulfV; last first.
  by rewrite expf_eq0 negb_and eq_sym (ltr_eqF xp) orbT.
have pnp : 0 < `|p`_n| by move: lcp; rewrite /lead_coef e es.
rewrite mulr1 -es mulrC -ler_pdivl_mulr //.
rewrite [_ / _]mulrC /cauchy_bound /lead_coef e -es /=.
move=> h1; apply: (ler_trans h1) => //.
rewrite ler_pmul2l ?invr_gt0 ?(ltrW pnp) // big_ord_recr /=.
rewrite es [_ + `|p`_m.+1|]addrC ler_paddl // ?normr_ge0 //.
rewrite big_ord_recr /= ler_add2r; apply: ler_sum => i.
rewrite normrM normrX.
rewrite -mulrA ler_pimulr ?normrE // ler_pdivr_mulr ?exprn_gt0 // mul1r.
by rewrite ler_eexpn2l // 1?ltrW //; case: i=> i hi /=; rewrite ltnW.
Qed.

Lemma le_cauchy_bound p : p != 0 -> {in `]-oo, (- cauchy_bound p)], noroot p}.
Proof.
move=> p_neq0 x; rewrite inE /= lerNgt; apply: contra => /rootP.
by move=> /(cauchy_boundP p_neq0) /ltr_normlP []; rewrite ltr_oppl.
Qed.
Hint Resolve le_cauchy_bound.

Lemma ge_cauchy_bound p : p != 0 -> {in `[cauchy_bound p, +oo[, noroot p}.
Proof.
move=> p_neq0 x; rewrite inE andbT /= lerNgt; apply: contra => /rootP.
by move=> /(cauchy_boundP p_neq0) /ltr_normlP []; rewrite ltr_oppl.
Qed.
Hint Resolve ge_cauchy_bound.

Lemma cauchy_bound_gt0 p : cauchy_bound p > 0.
Proof.
rewrite ltr_spaddl ?ltr01 ?mulr_ge0 ?invr_ge0 ?normr_ge0 //.
by rewrite sumr_ge0 // => i; rewrite normr_ge0.
Qed.
Hint Resolve cauchy_bound_gt0.

Lemma cauchy_bound_ge0 p : cauchy_bound p >= 0.
Proof. by rewrite ltrW. Qed.
Hint Resolve cauchy_bound_ge0.

End CauchyBound.

End PolyRealField.

Section PolyRCF.

Variable R : rcfType.

Section Prelim.

Implicit Types a b c : R.
Implicit Types x y z t : R.
Implicit Types p q r : {poly R}.


Lemma poly_ivt (p : {poly R}) (a b : R) :
  a <= b -> 0 \in `[p.[a], p.[b]] -> { x : R | x \in `[a, b] & root p x }.
Proof. by move=> leab root_p_ab; apply/sig2W/poly_ivt. Qed.

Lemma polyrN0_itv (i : interval R) (p : {poly R}) :
    {in i, noroot p} ->
  forall y x : R, y \in i -> x \in i -> sgr p.[x] = sgr p.[y].
Proof.
move=> hi y x hy hx; wlog xy: x y hx hy / x <= y=> [hwlog|].
  by case/orP: (ler_total x y)=> xy; [|symmetry]; apply: hwlog.
have hxyi: {subset `[x, y] <= i}.
  move=> z; apply: subitvP=> /=.
  by case: i hx hy {hi}=> [[[] ?|] [[] ?|]] /=; do ?[move/itvP->|move=> ?].
do 2![case: sgrP; first by move/rootP; rewrite (negPf (hi _ _))]=> //.
  move=> /ltrW py0 /ltrW p0x; case: (@poly_ivt (- p) x y)=> //.
    by rewrite inE !hornerN !oppr_cp0 p0x.
  by move=> z hz; rewrite rootN (negPf (hi z _)) // hxyi.
move=> /ltrW p0y /ltrW px0; case: (@poly_ivt p x y); rewrite ?inE ?px0 //.
by move=> z hz; rewrite (negPf (hi z _)) // hxyi.
Qed.

Lemma poly_div_factor (a : R) (P : {poly R} -> Prop) :
    (forall k, P k%:P) ->
    (forall p n k, p.[a] != 0 -> P p -> P (p * ('X - a%:P)^+(n.+1) + k%:P)%R)
  -> forall p, P p.
Proof.
move=> Pk Pq p.
move: {-2}p (leqnn (size p)); elim: (size p)=> {p} [|n ihn] p spn.
  move: spn; rewrite leqn0 size_poly_eq0; move/eqP->; rewrite -polyC0.
  exact: Pk.
case: (leqP (size p) 1)=> sp1; first by rewrite [p]size1_polyC ?sp1//.
rewrite (Pdiv.IdomainMonic.divp_eq (monicXsubC a) p).
rewrite [_ %% _]size1_polyC; last first.
  rewrite -ltnS.
  by rewrite (@leq_trans (size ('X - a%:P))) //
     ?ltn_modp ?polyXsubC_eq0 ?size_XsubC.
have [n' [q hqa hp]] := multiplicity_XsubC (p %/ ('X - a%:P)) a.
rewrite divpN0 ?size_XsubC ?polyXsubC_eq0 ?sp1 //= in hqa.
rewrite hp -mulrA -exprSr; apply: Pq=> //; apply: ihn.
rewrite (@leq_trans (size (q * ('X - a%:P) ^+ n'))) //.
  rewrite size_mul ?expf_eq0 ?polyXsubC_eq0 ?andbF //; last first.
    by apply: contra hqa; move/eqP->; rewrite root0.
  by rewrite size_exp_XsubC addnS leq_addr.
by rewrite -hp size_divp ?polyXsubC_eq0 ?size_XsubC // leq_subLR.
Qed.

Lemma nth_root x n : x > 0 -> { y | y > 0 & y ^+ (n.+1) = x }.
Proof.
move=> l0x.
case: (ltrgtP x 1)=> hx; last by exists 1; rewrite ?hx ?lter01// expr1n.
  case: (@poly_ivt ('X ^+ n.+1 - x%:P) 0 1); first by rewrite ler01.
    rewrite ?(hornerE,horner_exp) ?inE.
    by rewrite exprS mul0r sub0r expr1n oppr_cp0 subr_gte0/= !ltrW.
  move=> y; case/andP=> [l0y ly1]; rewrite rootE ?(hornerE,horner_exp).
  rewrite subr_eq0; move/eqP=> hyx; exists y=> //; rewrite lt0r l0y.
  rewrite andbT; apply/eqP=> y0; move: hyx; rewrite y0.
  by rewrite exprS mul0r=> x0; move: l0x; rewrite -x0 ltrr.
case: (@poly_ivt ('X ^+ n.+1 - x%:P) 0 x); first by rewrite ltrW.
  rewrite ?(hornerE,horner_exp) exprS mul0r sub0r ?inE.
  by rewrite oppr_cp0 (ltrW l0x) subr_ge0 ler_eexpr // ltrW.
move=> y; case/andP=> l0y lyx; rewrite rootE ?(hornerE,horner_exp).
rewrite subr_eq0; move/eqP=> hyx; exists y=> //; rewrite lt0r l0y.
rewrite andbT; apply/eqP=> y0; move: hyx; rewrite y0.
by rewrite exprS mul0r=> x0; move: l0x; rewrite -x0 ltrr.
Qed.

Lemma poly_cont x p e :
  e > 0 -> exists2 d, d > 0 & forall y, `|y - x| < d -> `|p.[y] - p.[x]| < e.
Proof.
elim/(@poly_div_factor x): p e.
  move=> e ep; exists 1; rewrite ?ltr01// => y hy.
  by rewrite !hornerC subrr normr0.
move=> p n k pxn0 Pp e ep.
case: (Pp (`|p.[x]|/2%:R)).
  by rewrite pmulr_lgt0 ?invr_gte0//= ?ltr0Sn// normrE.
move=> d' d'p He'.
case: (@nth_root (e / ((3%:R / 2%:R) * `|p.[x]|)) n).
  by rewrite ltr_pdivl_mulr ?mul0r ?pmulr_rgt0 ?invr_gt0 ?normrE ?ltr0Sn.
move=> d dp rootd.
exists (minr d d'); first by rewrite ltr_minr dp.
move=> y; rewrite ltr_minr; case/andP=> hxye hxye'.
rewrite !(hornerE, horner_exp) subrr [0 ^+ _]exprS mul0r mulr0 add0r addrK.
rewrite normrM (@ler_lt_trans _ (`|p.[y]| * d ^+ n.+1)) //.
  by rewrite ler_wpmul2l ?normrE // normrX ler_expn2r -?topredE /= ?normrE 1?ltrW.
rewrite rootd mulrCA gtr_pmulr //.
rewrite ltr_pdivr_mulr ?mul1r ?pmulr_rgt0 ?invr_gt0 ?ltr0Sn ?normrE //.
rewrite mulrDl mulrDl divff; last by rewrite -mulr2n pnatr_eq0.
rewrite !mul1r mulrC -ltr_subl_addr.
by rewrite (ler_lt_trans _ (He' y _)) // ler_sub_dist.
Qed.

Lemma poly_ltsp_roots p (rs : seq R) :
  (size rs >= size p)%N -> uniq rs -> all (root p) rs -> p = 0.
Proof.
move=> hrs urs rrs; apply/eqP; apply: contraLR hrs=> np0.
by rewrite -ltnNge; apply: max_poly_roots.
Qed.

Lemma ivt_sign (p : {poly R}) (a b : R) :
  a <= b -> sgr p.[a] * sgr p.[b] = -1 -> { x : R | x \in `]a, b[ & root p x}.
Proof.
move=> hab /eqP; rewrite mulrC mulr_sg_eqN1=> /andP [spb0 /eqP spb].
 case: (@poly_ivt (sgr p.[b] *: p) a b)=> //.
  by rewrite !hornerZ {1}spb mulNr -!normrEsg inE /= oppr_cp0 !normrE.
move=> c hc; rewrite rootZ ?sgr_eq0 // => rpc; exists c=> //.
rewrite inE /= !ltr_neqAle andbCA -!andbA [_ && (_ <= _)]hc andbT.
rewrite eq_sym -negb_or.
apply/negP=> /orP [] /eqP ec; move: rpc; rewrite -ec /root ?(negPf spb0) //.
by rewrite -sgr_cp0 -[sgr _]opprK -spb eqr_oppLR oppr0 sgr_cp0 (negPf spb0).
Qed.

Let rolle_weak a b p :
     a < b -> p.[a] = 0 -> p.[b] = 0 ->
   {c | (c \in `]a, b[) & (p^`().[c] == 0) || (p.[c] == 0)}.
Proof.
move=> lab pa0 pb0; apply/sig2W.
case p0: (p == 0).
  rewrite (eqP p0); exists (mid a b); first by rewrite mid_in_itv.
  by rewrite derivC horner0 eqxx.
have [n [p' p'a0 hp]] := multiplicity_XsubC p a; rewrite p0 /= in p'a0.
case: n hp pa0 p0 pb0 p'a0=> [ | n -> _ p0 pb0 p'a0].
  by rewrite {1}expr0 mulr1 rootE=> ->; move/eqP->.
have [m [q qb0 hp']] := multiplicity_XsubC p' b.
rewrite (contraNneq _ p'a0) /= in qb0 => [|->]; last exact: root0.
case: m hp' pb0 p0 p'a0 qb0=> [|m].
  rewrite {1}expr0 mulr1=> ->; move/eqP.
  rewrite !(hornerE, horner_exp, mulf_eq0).
  by rewrite !expf_eq0 !subr_eq0 !(gtr_eqF lab) !andbF !orbF !rootE=> ->.
move=> -> _ p0 p'a0 qb0; case: (sgrP (q.[a] * q.[b])); first 2 last.
- move=> sqasb; case: (@ivt_sign q a b)=> //; first exact: ltrW.
    by apply/eqP; rewrite -sgrM sgr_cp0.
  move=> c lacb rqc; exists c=> //.
  by rewrite !hornerM (eqP rqc) !mul0r eqxx orbT.
- move/eqP; rewrite mulf_eq0 (rootPf qb0) orbF; move/eqP=> qa0.
  by move: p'a0; rewrite ?rootM rootE qa0 eqxx.
- move=> hspq; rewrite !derivCE /= !mul1r mulrDl !pmulrn.
  set xan := (('X - a%:P) ^+ n); set xbm := (('X - b%:P) ^+ m).
  have ->: ('X - a%:P) ^+ n.+1 = ('X - a%:P) * xan by rewrite exprS.
  have ->: ('X - b%:P) ^+ m.+1 = ('X - b%:P) * xbm by rewrite exprS.
  rewrite -mulrzl -[_ *~ n.+1]mulrzl.
  have fac : forall x y z : {poly R}, x * (y * xbm) * (z * xan)
    = (y * z * x) * (xbm * xan).
    by move=> x y z; rewrite mulrCA !mulrA [_ * y]mulrC mulrA.
  rewrite !fac -!mulrDl; set r := _ + _ + _.
  case: (@ivt_sign (sgr q.[b] *: r) a b); first exact: ltrW.
    rewrite !hornerZ !sgr_smul mulrACA -expr2 sqr_sg (rootPf qb0) mul1r.
    rewrite !(subrr, mul0r, mulr0, addr0, add0r, hornerC, hornerXsubC,
      hornerD, hornerN, hornerM, hornerMn).
    rewrite [_ * _%:R]mulrC -!mulrA !pmulrn !mulrzl !sgrMz -sgrM.
    rewrite mulrAC mulrA -mulrA sgrM -opprB mulNr sgrN sgrM.
    by rewrite !gtr0_sg ?subr_gt0 ?mulr1 // mulrC.
move=> c lacb; rewrite rootE hornerZ mulf_eq0.
rewrite sgr_cp0 (rootPf qb0) orFb=> rc0.
by exists c=> //; rewrite !hornerM !mulf_eq0 rc0.
Qed.

Theorem rolle a b p :
  a < b -> p.[a] = p.[b] -> {c | c \in `]a, b[ & p^`().[c] = 0}.
Proof.
move=> lab pab.
wlog pb0 : p pab / p.[b] = 0 => [hwlog|].
  case: (hwlog (p - p.[b]%:P)); rewrite ?hornerE ?pab ?subrr //.
  by move=> c acb; rewrite derivE derivC subr0=> hc; exists c.
move: pab; rewrite pb0=> pa0.
have: (forall rs : seq R, {subset rs <= `]a, b[} ->
    (size p <= size rs)%N -> uniq rs -> all (root p) rs -> p = 0).
  by move=> rs hrs; apply: poly_ltsp_roots.
elim: (size p) a b lab pa0 pb0=> [|n ihn] a b lab pa0 pb0 max_roots.
  rewrite (@max_roots [::]) //=.
  by exists (mid a b); rewrite ?mid_in_itv // derivE horner0.
case: (@rolle_weak a b p); rewrite // ?pa0 ?pb0 //=.
move=> c hc; case: (altP (_ =P 0))=> //= p'c0 pc0; first by exists c.
suff: { d : R | d \in `]a, c[ & (p^`()).[d] = 0 }.
  case=> [d hd] p'd0; exists d=> //.
  by apply: subitvPr hd; rewrite //= (itvP hc).
apply: ihn=> //; first by rewrite (itvP hc).
  exact/eqP.
move=> rs hrs srs urs rrs; apply: (max_roots (c :: rs))=> //=; last exact/andP.
  move=> x; rewrite in_cons; case/predU1P=> hx; first by rewrite hx.
  have: x \in `]a, c[ by apply: hrs.
  by apply: subitvPr; rewrite /= (itvP hc).
by rewrite urs andbT; apply/negP; move/hrs; rewrite bound_in_itv.
Qed.

Theorem mvt a b p :
  a < b -> {c | c \in `]a, b[ & p.[b] - p.[a] = p^`().[c] * (b - a)}.
Proof.
move=> lab.
pose q := (p.[b] - p.[a])%:P * ('X - a%:P) - (b - a)%:P * (p - p.[a]%:P).
case: (@rolle a b q)=> //.
  by rewrite /q !hornerE !(subrr,mulr0) mulrC subrr.
move=> c lacb q'x0; exists c=> //.
move: q'x0; rewrite /q !derivE !(mul0r,add0r,subr0,mulr1).
by move/eqP; rewrite !hornerE mulrC subr_eq0; move/eqP.
Qed.

Lemma deriv_sign a b p :
  (forall x, x \in `]a, b[ -> p^`().[x] >= 0)
  -> (forall x y, (x \in `]a, b[) && (y \in `]a, b[)
    -> x < y -> p.[x] <= p.[y] ).
Proof.
move=> Pab x y; case/andP=> hx hy xy.
rewrite -subr_gte0; case: (@mvt x y p)=> //.
move=> c hc ->; rewrite pmulr_lge0 ?subr_gt0 ?Pab //.
by apply: subitvP hc; rewrite //= ?(itvP hx) ?(itvP hy).
Qed.

End Prelim.

Section MonotonictyAndRoots.

Section NoRoot.

Variable (p : {poly R}).

Variables (a b : R).

Hypothesis der_pos : forall x, x \in `]a, b[ -> (p^`()).[x] > 0.

Lemma derp0r : 0 <= p.[a] -> forall x, x \in `]a, b] -> p.[x] > 0.
Proof.
move=> pa0 x; case/itv_dec=> ax xb; case: (mvt p ax) => c acx.
move/(canRL (@subrK _ _))->; rewrite ltr_paddr //.
by rewrite pmulr_rgt0 ?subr_gt0 // der_pos //; apply: subitvPr acx.
Qed.

Lemma derppr : 0 < p.[a] -> forall x, x \in `[a, b] -> p.[x] > 0.
Proof.
move=> pa0 x hx; case exa: (x == a); first by rewrite (eqP exa).
case: (@mvt a x p); first by rewrite ltr_def exa (itvP hx).
move=> c hc; move/eqP; rewrite subr_eq; move/eqP->; rewrite ltr_spsaddr //.
rewrite pmulr_rgt0 ?subr_gt0 //; first by rewrite ltr_def exa (itvP hx).
by rewrite der_pos // (subitvPr _ hc) //= ?(itvP hx).
Qed.

Lemma derp0l : p.[b] <= 0 -> forall x, x \in `[a, b[ -> p.[x] < 0.
Proof.
move=> pb0 x hx; rewrite -oppr_gte0 /=.
case: (@mvt x b p)=> //; first by rewrite (itvP hx).
move=> c hc; move/(canRL (@addKr _ _))->; rewrite ltr_spaddr ?oppr_ge0 //.
rewrite pmulr_rgt0 // ?subr_gt0 ?(itvP hx) //.
by rewrite der_pos // (subitvPl _ hc) //= (itvP hx).
Qed.

Lemma derpnl : p.[b] < 0 -> forall x, x \in `[a, b] -> p.[x] < 0.
Proof.
move=> pbn x hx; case xb: (b == x) pbn; first by rewrite -(eqP xb).
case: (@mvt x b p); first by rewrite ltr_def xb ?(itvP hx).
move=> y hy; move/eqP; rewrite subr_eq; move/eqP->.
rewrite !ltrNge; apply: contra=> hpx; rewrite ler_paddr // ltrW //.
rewrite pmulr_rgt0 ?subr_gt0 ?(itvP hy) //.
by rewrite der_pos // (subitvPl _ hy) //= (itvP hx).
Qed.

End NoRoot.

Section NoRoot_sg.

Variable (p : {poly R}).

Variables (a b c : R).

Hypothesis derp_neq0 : {in `]a, b[, noroot p^`()}.
Hypothesis acb : c \in `]a, b[.

Local Notation sp'c := (sgr p^`().[c]).
Local Notation q := (sp'c *: p).

Fact derq_pos x : x \in `]a, b[ -> (q^`()).[x] > 0.
Proof.
move=> hx; rewrite derivZ hornerZ -sgr_cp0.
rewrite sgrM sgr_id mulr_sg_eq1 derp_neq0 //=.
by apply/eqP; apply: (@polyrN0_itv `]a, b[).
Qed.

Fact sgp x : sgr p.[x] = sp'c * sgr q.[x].
Proof.
by rewrite hornerZ sgr_smul mulrA -expr2 sqr_sg derp_neq0 ?mul1r.
Qed.

Fact hsgp x : 0 < q.[x] -> sgr p.[x] = sp'c.
Proof. by rewrite -sgr_cp0 sgp => /eqP->; rewrite mulr1. Qed.

Fact hsgpN x : q.[x] < 0 -> sgr p.[x] = - sp'c.
Proof. by rewrite -sgr_cp0 sgp => /eqP->; rewrite mulrN1. Qed.

Lemma ders0r : p.[a] = 0 -> forall x, x \in `]a, b] -> sgr p.[x] = sp'c.
Proof.
move=> pa0 x hx; rewrite hsgp // (@derp0r _ a b) //; first exact: derq_pos.
by rewrite hornerZ pa0 mulr0.
Qed.

Lemma derspr : sgr p.[a] = sp'c -> forall x, x \in `[a, b] -> sgr p.[x] = sp'c.
Proof.
move=> spa x hx; rewrite hsgp // (@derppr _ a b) //; first exact: derq_pos.
by rewrite -sgr_cp0 hornerZ sgrM sgr_id spa -expr2 sqr_sg derp_neq0.
Qed.

Lemma ders0l : p.[b] = 0 -> forall x, x \in `[a, b[ -> sgr p.[x] = -sp'c.
Proof.
move=> pa0 x hx; rewrite hsgpN // (@derp0l _ a b) //; first exact: derq_pos.
by rewrite hornerZ pa0 mulr0.
Qed.

Lemma derspl :
  sgr p.[b] = -sp'c -> forall x, x \in `[a, b] -> sgr p.[x] = -sp'c.
Proof.
move=> spb x hx; rewrite hsgpN // (@derpnl _ a b) //; first exact: derq_pos.
by rewrite -sgr_cp0 hornerZ sgr_smul spb mulrN -expr2 sqr_sg derp_neq0.
Qed.

End NoRoot_sg.

Variable (p : {poly R}).

Variables (a b : R).

Section der_root.

Hypothesis der_pos : forall x, x \in `]a, b[ -> (p^`()).[x] > 0.

Lemma derp_root : a <= b -> 0 \in `]p.[a], p.[b][ ->
  { r : R |
    [/\ forall x, x \in `[a, r[ -> p.[x] < 0,
      p.[r] = 0,
      r \in `]a, b[ &
      forall x, x \in `]r, b] -> p.[x] > 0] }.
Proof.
move=> leab hpab.
have /eqP hs : sgr p.[a] * sgr p.[b] == -1.
  by rewrite -sgrM sgr_cp0 pmulr_llt0 ?(itvP hpab).
case: (ivt_sign leab hs) => r arb pr0; exists r; split => //; last 2 first.
- by move/eqP: pr0.
- move=> x rxb; have hd : forall t, t \in `]r, b[ -> 0 < (p^`()).[t].
    by move=> t ht; rewrite der_pos // ?(subitvPl _ ht) //= ?(itvP arb).
  by rewrite (derp0r hd) ?(eqP pr0).
- move=> x rxb; have hd : forall t, t \in `]a, r[ -> 0 < (p^`()).[t].
    by move=> t ht; rewrite der_pos // ?(subitvPr _ ht) //= ?(itvP arb).
  by rewrite (derp0l hd) ?(eqP pr0).
Qed.

End der_root.





End MonotonictyAndRoots.

Section RootsOn.

Variable T : predType R.

Definition roots_on (p : {poly R}) (i : T) (s : seq R) :=
  forall x, (x \in i) && (root p x) = (x \in s).

Lemma roots_onP p i s : roots_on p i s -> {in i, root p =1 mem s}.
Proof. by move=> hp x hx; move: (hp x); rewrite hx. Qed.

Lemma roots_on_in p i s :
  roots_on p i s -> forall x, x \in s -> x \in i.
Proof. by move=> hp x; rewrite -hp; case/andP. Qed.

Lemma roots_on_root p i s :
  roots_on p i s -> forall x, x \in s -> root p x.
Proof. by move=> hp x; rewrite -hp; case/andP. Qed.

Lemma root_roots_on p i s :
  roots_on p i s -> forall x, x \in i -> root p x -> x \in s.
Proof. by move=> hp x; rewrite -hp=> ->. Qed.

Lemma roots_on_opp p i s : roots_on (- p) i s -> roots_on p i s.
Proof. by move=> hp x; rewrite -hp rootN. Qed.

Lemma roots_on_nil p i : roots_on p i [::] -> {in i, noroot p}.
Proof. by move=> hp x hx; move: (hp x); rewrite in_nil hx /=; move->. Qed.

Lemma roots_on_same s' p i s : s =i s' -> (roots_on p i s <-> roots_on p i s').
Proof. by move=> hss'; split=> hs x; rewrite (hss', (I, hss')). Qed.

End RootsOn.






Lemma roots_on_comp p a b s :
  roots_on (p \Po (-'X)) `](-b), (-a)[ (map (-%R) s) <-> roots_on p `]a, b[ s.
Proof.
split=> /= hs x; rewrite ?root_comp ?hornerE.
  move: (hs (-x)); rewrite mem_map; last exact: (inv_inj (@opprK _)).
  by rewrite root_comp ?hornerE oppr_itv !opprK.
rewrite -[x]opprK oppr_itv /= mem_map; last exact: (inv_inj (@opprK _)).
by move: (hs (-x)); rewrite !opprK.
Qed.

Lemma min_roots_on p a b x s :
    all (> x) s -> roots_on p `]a, b[ (x :: s) ->
  [/\ x \in `]a, b[, roots_on p `]a, x[ [::], root p x & roots_on p `]x, b[ s].
Proof.
move=> lxs hxs.
have hx: x \in `]a, b[ by rewrite (roots_on_in hxs) ?mem_head.
rewrite hx (roots_on_root hxs) ?mem_head //.
split=> // y; move: (hxs y); rewrite ?in_nil ?in_cons /=.
  case hy: (y \in `]a, x[)=> //=.
  rewrite (subitvPr _ hy) //= ?(itvP hx) //= => ->.
  rewrite ltr_eqF ?(itvP hy) //=; apply/negP.
  by move/allP: lxs=> lxs /lxs; rewrite ltrNge ?(itvP hy).
move/allP:lxs=>lxs; case eyx: (y == _)=> /=.
  case/andP=> hy _; rewrite (eqP eyx).
  rewrite boundl_in_itv /=; symmetry.
  by apply/negP; move/lxs; rewrite ltrr.
case py0: root; rewrite !(andbT, andbF) //.
case ys: (y \in s); first by move/lxs:ys; rewrite ?inE => ->; case/andP.
move/negP; move/negP=> nhy; apply: negbTE; apply: contra nhy.
by apply: subitvPl; rewrite //= ?(itvP hx).
Qed.

Lemma max_roots_on p a b x s :
    all (< x) s -> roots_on p `]a, b[ (x :: s) ->
  [/\ x \in `]a, b[, roots_on p `]x, b[ [::], root p x & roots_on p `]a, x[ s].
Proof.
move/allP=> lsx /roots_on_comp/=/min_roots_on[].
  apply/allP=> y; rewrite -[y]opprK mem_map.
    by move/lsx; rewrite ltr_oppr opprK.
  exact: (inv_inj (@opprK _)).
rewrite oppr_itv root_comp !hornerE !opprK=> -> rxb -> rax.
by split=> //; apply/roots_on_comp.
Qed.

Lemma roots_on_cons p a b r s :
  sorted <%R (r :: s) -> roots_on p `]a, b[ (r :: s) -> roots_on p `]r, b[ s.
Proof.
move=> /= hrs hr.
have:= (order_path_min (@ltr_trans _) hrs)=> allrs.
by case: (min_roots_on allrs hr).
Qed.

Lemma roots_on_rcons : forall p a b r s,
  sorted <%R (rcons s r) -> roots_on p `]a, b[ (rcons s r)
  -> roots_on p `]a, r[ s.
Proof.
move=> p a b r s; rewrite -{1}[s]revK -!rev_cons rev_sorted /=.
move=> hrs hr.
have := (order_path_min (rev_trans (@ltr_trans _)) hrs)=> allrrs.
have allrs: (all (< r) s).
  by apply/allP=> x hx; move/allP:allrrs; apply; rewrite mem_rev.
move/(@roots_on_same _ _ _ _ (r::s)):hr=>hr.
case: (max_roots_on allrs (hr _))=> //.
by move=> x; rewrite mem_rcons.
Qed.


Lemma no_roots_on (p : {poly R}) a b :
  {in `]a, b[, noroot p} -> roots_on p `]a, b[ [::].
Proof.
move=> hr x; rewrite in_nil; case hx: (x \in _) => //=.
by apply: negPf; apply: hr hx.
Qed.

Lemma monotonic_rootN (p : {poly R}) (a b : R) :
    {in `]a, b[, noroot p^`()} ->
  ((roots_on p `]a, b[ [::]) + ({r : R | roots_on p `]a, b[ [:: r]}))%type.
Proof.
move=> hp'; case: (ltrP a b); last first => leab.
  by left => x; rewrite in_nil itv_gte.
wlog {hp'} hp'sg: p / forall x, x \in `]a, b[ -> sgr (p^`()).[x] = 1.
  move=> hwlog. have := (polyrN0_itv hp').
  move: (mid_in_itvoo leab)=> hm /(_ _ _ hm).
  case: (sgrP _.[mid a b])=> hpm.
  - by move=> norm; move: (hp' _ hm); rewrite rootE hpm eqxx.
  - by move/(hwlog p).
  - move=> hp'N; case: (hwlog (-p))=> [x|h|[r hr]].
    * by rewrite derivE hornerN sgrN=> /hp'N->; rewrite opprK.
    * by left; apply: roots_on_opp.
    * by right; exists r; apply: roots_on_opp.
have hp'pos: forall x, x \in `]a, b[ -> (p^`()).[x] > 0.
  by move=> x; move/hp'sg; move/eqP; rewrite sgr_cp0.
case: (lerP 0 p.[a]) => ha.
- left; apply: no_roots_on => x axb.
  by rewrite rootE gtr_eqF // (@derp0r _ a b) // (subitvPr _ axb) /=.
- case: (lerP p.[b] 0) => hb.
  + left => x; rewrite in_nil; apply: negbTE; case axb: (x \in `]a, b[) => //=.
    by rewrite rootE ltr_eqF // (@derp0l _ a b) // (subitvPl _ axb) /=.
  + case: (derp_root hp'pos (ltrW leab) _).
      by rewrite ?inE; apply/andP.
  move=> r [h1 h2 h3] h4; right.
  exists r => x; rewrite in_cons in_nil (itv_splitU2 h3).
  case exr: (x == r); rewrite ?(andbT, orbT, andbF, orbF) /=.
    by rewrite rootE (eqP exr) h2 eqxx.
  case px0: root; rewrite (andbT, andbF) //.
  move/eqP: px0=> px0; apply/negP; case/orP=> hx.
    by move: (h1 x); rewrite (subitvPl _ hx) //= px0 ltrr; move/implyP.
  by move: (h4 x); rewrite (subitvPr _ hx) //= px0 ltrr; move/implyP.
Qed.




Lemma cat_roots_on (p : {poly R}) a b x :
    x \in `]a, b[ -> ~~ (root p x) ->
    forall s s', sorted <%R s -> sorted <%R s' ->
    roots_on p `]a, x[ s -> roots_on p `]x, b[ s' ->
  roots_on p `]a, b[ (s ++ s').
Proof.
move=> hx /= npx0 s; elim: s a hx => [|y s ihs] a hx s' //= ss ss'.
  move/roots_on_nil=> hax hs' y.
  rewrite -hs'; case py0: root; rewrite ?(andbT, andbF) //.
  rewrite (itv_splitU2 hx); case: (y \in `]x, b[); rewrite ?orbF ?orbT //=.
  apply/negP; case/orP; first by move/hax; rewrite py0.
  by move/eqP=> exy; rewrite -exy py0 in npx0.
move/min_roots_on; rewrite order_path_min //; last exact: ltr_trans.
case=> // hy hay py0 hs hs' z.
rewrite in_cons; case ezy: (z == y)=> /=.
  by rewrite (eqP ezy) py0 andbT (subitvPr _ hy) //= ?(itvP hx).
rewrite -(ihs y) //; last exact: path_sorted ss; last first.
  by rewrite inE /= (itvP hx) (itvP hy).
case pz0: root; rewrite ?(andbT, andbF) //.
rewrite (@itv_splitU2 _ y); last by rewrite (subitvPr _ hy) //= (itvP hx).
rewrite ezy /=; case: (z \in `]y, b[); rewrite ?orbF ?orbT //.
by apply/negP=> hz; move: (hay z); rewrite hz pz0 in_nil.
Qed.

CoInductive roots_spec (p : {poly R}) (i : pred R) (s : seq R) :
  {poly R} -> bool -> seq R -> Type :=
| Roots0 of p = 0 :> {poly R} & s = [::] : roots_spec p i s 0 true [::]
| Roots of p != 0 & roots_on p i s
  & sorted <%R s : roots_spec p i s p false s.

Lemma itv_roots (p :{poly R}) (a b : R) :
  {s : seq R & roots_spec p (topred `]a, b[) s p (p == 0) s}.
Proof.
case p0: (_ == 0).
  by rewrite (eqP p0); exists [::]; constructor.
elim: (size p) {-2}p (leqnn (size p)) p0 a b => {p} [| n ihn] p sp p0 a b.
   by exists [::]; move: p0; rewrite -size_poly_eq0 -leqn0 sp.
move/negbT: (p0)=> np0.
case p'0 : (p^`() == 0).
  move: p'0; rewrite -derivn1 -derivn_poly0; move/size1_polyC => pC.
  exists [::]; constructor=> // x; rewrite in_nil pC rootC; apply: negPf.
  by rewrite negb_and -polyC_eq0 -pC p0 orbT.
move/negbT: (p'0) => np'0.
have sizep' : (size p^`() <= n)%N.
  rewrite -ltnS; apply: leq_trans sp; rewrite size_deriv prednK // lt0n.
  by rewrite size_poly_eq0 p0.
case: (ihn _ sizep' p'0 a b) => sp' ih {ihn}.
case ltab : (a < b); last first.
  exists [::]; constructor=> // x; rewrite in_nil.
  case axb : (x \in _) => //=.
  by case/andP: axb => ax xb; move: ltab; rewrite (ltr_trans ax xb).
elim: sp' a b ltab ih => [|r1 sp' hsp'] a b ltab hp'.
  case: hp' np'0; rewrite ?eqxx // => np'0 hroots' _ _.
  move/roots_on_nil : hroots' => hroots'.
  case: (monotonic_rootN hroots') => [h| [r rh]].
    by exists [::]; constructor.
  by exists [:: r]; constructor=> //=; rewrite andbT.
case: hp' np'0; rewrite ?eqxx // => np'0 hroots' /= hpath' _.
case: (min_roots_on _ hroots').
  by rewrite order_path_min //; apply: ltr_trans.
move=> hr1 har1 p'r10 hr1b.
case: (hsp' r1 b); first by rewrite (itvP hr1).
  by constructor=> //; rewrite (path_sorted hpath').
move=> s spec_s.
case: spec_s np0; rewrite ?eqxx //.
move=> np0 hroot hsort _.
move: (roots_on_nil har1).
case pr1 : (root p r1); case/monotonic_rootN => hrootsl; last 2 first.
- exists s; constructor=> //.
  by rewrite -[s]cat0s; apply: (cat_roots_on hr1)=> //; rewrite pr1.
- case: hrootsl=> r hr; exists (r::s); constructor=> //=.
    by rewrite -cat1s; apply: (cat_roots_on hr1)=> //; rewrite pr1.
  rewrite path_min_sorted // => y; rewrite -hroot; case/andP=> hy _.
  rewrite (@ltr_trans _ r1) ?(itvP hy) //.
  by rewrite (itvP (roots_on_in hr (mem_head _ _))).
- exists (r1::s); constructor=> //=; last first.
    rewrite path_min_sorted=> // y; rewrite -hroot.
    by case/andP; move/itvP->.
  move=> x; rewrite in_cons; case exr1: (x == r1)=> /=.
    by rewrite (eqP exr1) pr1 andbT.
  rewrite -hroot; case px: root; rewrite ?(andbT, andbF) //.
  rewrite (itv_splitU2 hr1) exr1 /=.
  case: (_ \in `]r1, _[); rewrite ?(orbT, orbF) //.
  by apply/negP=> hx; move: (hrootsl x); rewrite hx px in_nil.
- case: hrootsl => r0 hrootsl.
  move/min_roots_on:hrootsl; case=> // hr0 har0 pr0 hr0r1.
  exists [:: r0, r1 & s]; constructor=> //=; last first.
    rewrite (itvP hr0) /= path_min_sorted // => y.
    by rewrite -hroot; case/andP; move/itvP->.
  move=> y; rewrite !in_cons (itv_splitU2 hr1) (itv_splitU2 hr0).
  case eyr0: (y == r0); rewrite ?(orbT, orbF, orTb, orFb).
    by rewrite (eqP eyr0) pr0.
  case eyr1: (y == r1); rewrite ?(orbT, orbF, orTb, orFb).
    by rewrite (eqP eyr1) pr1.
  rewrite -hroot; case py0: root; rewrite ?(andbF, andbT) //.
  case: (_ \in `]r1, _[); rewrite ?(orbT, orbF) //.
  apply/negP; case/orP=> hy; first by move: (har0 y); rewrite hy py0 in_nil.
  by move: (hr0r1 y); rewrite hy py0 in_nil.
Qed.

Definition roots (p : {poly R}) a b := projT1 (itv_roots p a b).

Lemma rootsP p a b :
  roots_spec p (topred `]a, b[) (roots p a b) p (p == 0) (roots p a b).
Proof. by rewrite /roots; case hp: itv_roots. Qed.

Lemma roots0 a b : roots 0 a b = [::].
Proof. by case: rootsP=> //=; rewrite eqxx. Qed.

Lemma roots_on_roots : forall p a b, p != 0 ->
  roots_on p `]a, b[ (roots p a b).
Proof. by move=> a b p; case: rootsP. Qed.
Hint Resolve roots_on_roots.

Lemma sorted_roots a b p : sorted <%R (roots p a b).
Proof. by case: rootsP. Qed.
Hint Resolve sorted_roots.

Lemma path_roots p a b : path <%R a (roots p a b).
Proof.
case: rootsP=> //= p0 hp sp; rewrite path_min_sorted //.
by move=> y; rewrite -hp; case/andP; move/itvP->.
Qed.
Hint Resolve path_roots.

Lemma root_is_roots (p : {poly R}) (a b : R) :
   p != 0 -> forall x, x \in `]a, b[ -> root p x = (x \in roots p a b).
Proof. by case: rootsP=> // p0 hs ps _ y hy /=; rewrite -hs hy. Qed.

Lemma root_in_roots (p : {poly R}) a b :
  p != 0 -> forall x, x \in `]a, b[ -> root p x -> x \in (roots p a b).
Proof. by move=> p0 x axb rpx; rewrite -root_is_roots. Qed.

Lemma root_roots p a b x : x \in roots p a b -> root p x.
Proof. by case: rootsP=> // p0 <- _; case/andP. Qed.

Lemma roots_nil p a b : p != 0 ->
  roots p a b = [::] -> {in `]a, b[, noroot p}.
Proof.
case: rootsP => // p0 hs ps _ s0 x axb.
by move: (hs x); rewrite s0 in_nil !axb /= => ->.
Qed.

Lemma roots_in p a b x : x \in roots p a b -> x \in `]a, b[.
Proof. by case: rootsP=> //= np0 ron_p *; apply: (roots_on_in ron_p). Qed.

Lemma rootsEba p a b : b <= a -> roots p a b = [::].
Proof.
case: rootsP=> // p0; case: (roots _ _ _) => [|x s] hs ps ba //;
by move: (hs x); rewrite itv_gte //= mem_head.
Qed.

Lemma roots_on_uniq p a b s1 s2 :
    sorted <%R s1 -> sorted <%R s2 ->
  roots_on p `]a, b[ s1 -> roots_on p `]a, b[ s2 -> s1 = s2.
Proof.
elim: s1 p a b s2 => [| r1 s1 ih] p a b [| r2 s2] ps1 ps2 rs1 rs2 //.
- have rpr2 : root p r2 by apply: (roots_on_root rs2); rewrite mem_head.
  have abr2 : r2 \in `]a, b[ by apply: (roots_on_in rs2); rewrite mem_head.
  by have:= (rs1 r2); rewrite rpr2 !abr2 in_nil.
- have rpr1 : root p r1 by apply: (roots_on_root rs1); rewrite mem_head.
  have abr1 : r1 \in `]a, b[ by apply: (roots_on_in rs1); rewrite mem_head.
  by have:= (rs2 r1); rewrite rpr1 !abr1 in_nil.
- have er1r2 : r1 = r2.
    move: (rs1 r2); rewrite (roots_on_root rs2) ?mem_head //.
    rewrite !(roots_on_in rs2) ?mem_head //= in_cons.
    move/(@sym_eq _ true); case/orP => hr2; first by rewrite (eqP hr2).
    move: ps1=> /=; move/(order_path_min (@ltr_trans R)); move/allP.
    move/(_ r2 hr2) => h1.
    move: (rs2 r1); rewrite (roots_on_root rs1) ?mem_head //.
    rewrite !(roots_on_in rs1) ?mem_head //= in_cons.
    move/(@sym_eq _ true); case/orP => hr1; first by rewrite (eqP hr1).
    move: ps2=> /=; move/(order_path_min (@ltr_trans R)); move/allP.
    by move/(_ r1 hr1); rewrite ltrNge ltrW.
congr (_ :: _) => //; rewrite er1r2 in ps1 rs1.
have h3 := (roots_on_cons ps1 rs1).
have h4 := (roots_on_cons ps2 rs2).
move: ps1 ps2=> /=; move/path_sorted=> hs1; move/path_sorted=> hs2.
exact: (ih p _ b _ hs1 hs2 h3 h4).
Qed.

Lemma roots_eq (p q : {poly R}) (a b : R) :
    p != 0 -> q != 0 ->
  ({in `]a, b[, root p =1 root q} <-> roots p a b = roots q a b).
Proof.
move=> p0 q0.
case hab : (a < b); last first.
  split; first by rewrite !rootsEba // lerNgt hab.
  move=> _ x. rewrite !inE; case/andP=> ax xb.
  by move: hab; rewrite (@ltr_trans _ x) /=.
split=> hpq.
  apply: (@roots_on_uniq p a b); rewrite ?path_roots ?p0 ?q0 //.
    by apply: roots_on_roots.
  rewrite /roots_on => x; case hx: (_ \in _).
    by rewrite -hx hpq //; apply: roots_on_roots.
  by rewrite /= -(andFb (q.[x] == 0)) -hx; apply: roots_on_roots.
move=> x axb /=.
by rewrite (@root_is_roots q a b) // (@root_is_roots p a b) // hpq.
Qed.

Lemma roots_opp p : roots (- p) =2 roots p.
Proof.
move=> a b; case p0 : (p == 0); first by rewrite (eqP p0) oppr0.
by apply/roots_eq=> [||x]; rewrite ?oppr_eq0 ?p0 ?rootN.
Qed.

Lemma no_root_roots (p : {poly R}) a b :
  {in `]a, b[ , noroot p} -> roots p a b = [::].
Proof.
move=> hr; case: rootsP => // p0 hs ps.
apply: (@roots_on_uniq p a b)=> // x; rewrite in_nil.
by apply/negP; case/andP; move/hr; move/negPf->.
Qed.

Lemma head_roots_on_ge p a b s :
  a < b -> roots_on p `]a, b[ s -> a < head b s.
Proof.
case: s => [|x s] ab // /(_ x).
by rewrite in_cons eqxx; case/andP; case/andP.
Qed.

Lemma head_roots_ge : forall p a b, a < b -> a < head b (roots p a b).
Proof.
by move=> p a b; case: rootsP=> // *; apply: head_roots_on_ge.
Qed.

Lemma last_roots_on_le p a b s :
  a < b -> roots_on p `]a, b[ s -> last a s < b.
Proof.
case: s => [|x s] ab rs //.
by rewrite (itvP (roots_on_in rs _)) //= mem_last.
Qed.

Lemma last_roots_le p a b : a < b -> last a (roots p a b) < b.
Proof. by case: rootsP=> // *; apply: last_roots_on_le. Qed.

Lemma roots_uniq p a b s :
  p != 0 -> roots_on p `]a, b[ s -> sorted <%R s -> s = roots p a b.
Proof.
case: rootsP=> // p0 hs' ps' _ hs ss.
exact: (@roots_on_uniq p a b)=> //.
Qed.

Lemma roots_cons p a b x s :
  (roots p a b == x :: s)
    = [&& p != 0, x \in `]a, b[,
          roots p a x == [::], root p x & roots p x b == s].
Proof.
case: rootsP=> // p0 hs' ps' /=.
apply/idP/idP.
  move/eqP=> es'; move: ps' hs'; rewrite es' /= => sxs.
  case/min_roots_on; first by apply: order_path_min=> //; apply: ltr_trans.
  move=> -> rax px0 rxb.
  rewrite px0 (@roots_uniq p a x [::]) // (@roots_uniq p x b s) ?eqxx //=.
  by move/path_sorted:sxs.
case: rootsP p0=> // p0 rax sax _.
case/and3P=> hx hax; rewrite (eqP hax) in rax sax.
case: rootsP p0=> // p0 rxb sxb _.
case/andP=> px0 hxb; rewrite (eqP hxb) in rxb sxb.
rewrite [_ :: _](@roots_uniq p a b) //; last first.
  rewrite /= path_min_sorted // => y.
  by rewrite -(eqP hxb); move/roots_in; move/itvP->.
move=> y; rewrite (itv_splitU2 hx) !andb_orl in_cons.
case hy: (y == x); first by rewrite (eqP hy) px0 orbT.
by rewrite andFb orFb rax rxb in_nil.
Qed.

Lemma roots_rcons p a b x s :
  (roots p a b == rcons s x) =
    [&& p != 0, x \in `]a , b[,
        roots p x b == [::], root p x & roots p a x == s].
Proof.
case: rootsP; first by case: s.
move=> // p0 hs' ps' /=.
apply/idP/idP.
  move/eqP=> es'; move: ps' hs'; rewrite es' /= => sxs.
  have hsx: rcons s x =i x :: rev s.
    by move=> y; rewrite mem_rcons !in_cons mem_rev.
  move/(roots_on_same _ _ hsx).
  case/max_roots_on.
    move: sxs; rewrite -[rcons _ _]revK rev_sorted rev_rcons.
    by apply: order_path_min=> u v w /=; move/(ltr_trans _); apply.
  move=> -> rax px0 rxb.
  move/(@roots_on_same _ s): rxb; move/(_ (mem_rev _))=> rxb.
  rewrite px0 (@roots_uniq p x b [::]) // (@roots_uniq p a x s) ?eqxx //=.
  move: sxs; rewrite -[rcons _ _]revK rev_sorted rev_rcons.
  by move/path_sorted; rewrite -rev_sorted revK.
case: rootsP p0=> // p0 rax sax _.
case/and3P=> hx hax; rewrite (eqP hax) in rax sax.
case: rootsP p0=> // p0 rxb sxb _.
case/andP=> px0 hxb; rewrite (eqP hxb) in rxb sxb.
rewrite [rcons _ _](@roots_uniq p a b) //; last first.
  rewrite -[rcons _ _]revK rev_sorted rev_rcons /= path_min_sorted.
    by rewrite -rev_sorted revK.
  move=> y; rewrite mem_rev; rewrite -(eqP hxb).
  by move/roots_in; move/itvP->.
move=> y; rewrite (itv_splitU2 hx) mem_rcons in_cons !andb_orl.
case hy: (y == x); first by rewrite (eqP hy) px0 orbT.
by rewrite rxb rax in_nil !orbF.
Qed.

Section NeighborHood.

Implicit Types a b : R.

Implicit Types p : {poly R}.

Definition next_root (p : {poly R}) x b :=
  if p == 0 then x else head (maxr b x) (roots p x b).

Lemma next_root0 a b : next_root 0 a b = a.
Proof. by rewrite /next_root eqxx. Qed.

CoInductive next_root_spec (p : {poly R}) x b : bool -> R -> Type :=
| NextRootSpec0 of p = 0 : next_root_spec p x b true x
| NextRootSpecRoot y of p != 0 & p.[y] = 0 & y \in `]x, b[
  & {in `]x, y[, forall z, ~~(root p z)} : next_root_spec p x b true y
| NextRootSpecNoRoot c of p != 0 & c = maxr b x
  & {in `]x, b[, forall z, ~~(root p z)} : next_root_spec p x b (p.[c] == 0) c.

Lemma next_rootP (p : {poly R}) a b :
  next_root_spec p a b (p.[next_root p a b] == 0) (next_root p a b).
Proof.
rewrite /next_root /=; case hs: roots => [|x s] /=.
  case: (altP (p =P 0))=> p0.
    by rewrite {2}p0 hornerC eqxx; constructor; rewrite p0.
  by constructor=> // y hy; apply: (roots_nil p0 hs).
move/eqP: hs; rewrite roots_cons; case/and5P=> p0 hx; move/eqP=> rap rpx rx.
rewrite (negPf p0) (rootPt rpx); constructor=> //; first by move/eqP: rpx.
by move=> y hy /=; move/(roots_nil p0): (rap); apply.
Qed.

Lemma next_root_in p a b : next_root p a b \in `[a, maxr b a].
Proof.
case: next_rootP => [p0|y np0 py0 hy _|c np0 hc _].
* by rewrite bound_in_itv /= ler_maxr lerr orbT.
* by apply: subitvP hy=> /=; rewrite ler_maxr !lerr.
* by rewrite hc bound_in_itv /= ler_maxr lerr orbT.
Qed.

Lemma next_root_gt p a b : a < b -> p != 0 -> next_root p a b > a.
Proof.
move=> ab np0; case: next_rootP=> [p0|y _ py0 hy _|c _ -> _].
* by rewrite p0 eqxx in np0.
* by rewrite (itvP hy).
* by rewrite maxr_l // ltrW.
Qed.

Lemma next_noroot p a b : {in `]a, (next_root p a b)[, noroot p}.
Proof.
move=> z; case: next_rootP; first by rewrite itv_xx.
  by move=> y np0 py0 hy hp hz; rewrite (negPf (hp _ _)).
move=> c p0 -> hp hz; rewrite (negPf (hp _ _)) //.
by case: maxrP hz; last by rewrite itv_xx.
Qed.

Lemma is_next_root p a b x :
  next_root_spec p a b (root p x) x -> x = next_root p a b.
Proof.
case; first by move->; rewrite /next_root eqxx.
  move=> y; case: next_rootP; first by move->; rewrite eqxx.
  move=> y' np0 py'0 hy' hp' _ py0 hy hp.
    wlog: y y' hy' hy hp' hp py0 py'0 / y <= y'.
      by case/orP: (ler_total y y')=> lyy' hw; [|symmetry]; apply: hw.
    case: ltrgtP=> // hyy' _; move: (hp' y).
    by rewrite rootE py0 eqxx inE /= (itvP hy) hyy'; move/(_ isT).
  move=> c p0 ->; case: maxrP=> hab; last by rewrite itv_gte //= ltrW.
  by move=> hpz _ py0 hy; move/hpz:hy; rewrite rootE py0 eqxx.
case: next_rootP => //; first by move->; rewrite eqxx.
  by move=> y np0 py0 hy _ c _ _; move/(_ _ hy); rewrite rootE py0 eqxx.
by move=> c _ -> _ c' _ ->.
Qed.

Definition prev_root (p : {poly R}) a x :=
  if p == 0 then x else last (minr a x) (roots p a x).

Lemma prev_root0 a b : prev_root 0 a b = b.
Proof. by rewrite /prev_root eqxx. Qed.

CoInductive prev_root_spec (p : {poly R}) a x : bool -> R -> Type :=
| PrevRootSpec0 of p = 0 : prev_root_spec p a x true x
| PrevRootSpecRoot y of p != 0 & p.[y] = 0 & y \in`]a, x[
  & {in `]y, x[, forall z, ~~(root p z)} : prev_root_spec p a x true y
| PrevRootSpecNoRoot c of p != 0 & c = minr a x
 & {in `]a, x[, forall z, ~~(root p z)} : prev_root_spec p a x (p.[c] == 0) c.

Lemma prev_rootP (p : {poly R}) a b :
  prev_root_spec p a b (p.[prev_root p a b] == 0) (prev_root p a b).
Proof.
rewrite /prev_root /=; move hs: (roots _ _ _)=> s.
case: (lastP s) hs=> {s} [|s x] hs /=.
  case: (altP (p =P 0))=> p0.
    by rewrite {2}p0 hornerC eqxx; constructor; rewrite p0.
  by constructor=> // y hy; apply: (roots_nil p0 hs).
rewrite last_rcons; move/eqP: hs.
rewrite roots_rcons; case/and5P=> p0 hx; move/eqP=> rap rpx rx.
rewrite (negPf p0) (rootPt rpx); constructor=> //; first by move/eqP: rpx.
by move=> y hy /=; move/(roots_nil p0): (rap); apply.
Qed.

Lemma prev_root_in p a b : prev_root p a b \in `[minr a b, b].
Proof.
case: prev_rootP => [p0|y np0 py0 hy _|c np0 hc _].
* by rewrite bound_in_itv /= ler_minl lerr orbT.
* by apply: subitvP hy=> /=; rewrite ler_minl !lerr.
* by rewrite hc bound_in_itv /= ler_minl lerr orbT.
Qed.

Lemma prev_noroot p a b : {in `](prev_root p a b), b[, noroot p}.
Proof.
move=> z; case: prev_rootP; first by rewrite itv_xx.
  by move=> y np0 py0 hy hp hz; rewrite (negPf (hp _ _)).
move=> c np0 ->; case: minrP=> hab; last by rewrite itv_xx.
by move=> hp hz; rewrite (negPf (hp _ _)).
Qed.

Lemma prev_root_lt p a b : a < b -> p != 0 -> prev_root p a b < b.
Proof.
move=> ab np0; case: prev_rootP=> [p0|y _ py0 hy _|c _ -> _].
* by rewrite p0 eqxx in np0.
* by rewrite (itvP hy).
* by rewrite minr_l // ltrW.
Qed.

Lemma is_prev_root p a b x :
  prev_root_spec p a b (root p x) x -> x = prev_root p a b.
Proof.
case; first by move->; rewrite /prev_root eqxx.
  move=> y; case: prev_rootP; first by move->; rewrite eqxx.
  move=> y' np0 py'0 hy' hp' _ py0 hy hp.
    wlog: y y' hy' hy hp' hp py0 py'0 / y <= y'.
      by case/orP: (ler_total y y')=> lyy' hw; [|symmetry]; apply: hw.
    case: ltrgtP=> // hyy' _; move/implyP: (hp y').
    by rewrite rootE py'0 eqxx inE /= (itvP hy') hyy'.
  by move=> c _ _ hpz _ py0 hy; move/hpz:hy; rewrite rootE py0 eqxx.
case: prev_rootP=> //; first by move->; rewrite eqxx.
  move=> y ? py0 hy _ c _ ->; case: minrP hy=> hab; last first.
    by rewrite itv_gte //= ltrW.
  by move=> hy; move/(_ _ hy); rewrite rootE py0 eqxx.
by move=> c _ -> _ c' _ ->.
Qed.

Definition neighpr p a b := `]a, (next_root p a b)[.

Definition neighpl p a b := `](prev_root p a b), b[.

Lemma neighpl_root p a x : {in neighpl p a x, noroot p}.
Proof. exact: prev_noroot. Qed.

Lemma sgr_neighplN p a x :
  ~~ root p x -> {in neighpl p a x, forall y, (sgr p.[y] = sgr p.[x])}.
Proof.
rewrite /neighpl=> nrpx /= y hy.
apply: (@polyrN0_itv `[y, x]); do ?by rewrite bound_in_itv /= (itvP hy).
move=> z; rewrite (@itv_splitU _ x false) ?itv_xx /=; last first.
  by rewrite bound_in_itv /= (itvP hy).
rewrite orbC => /predU1P[-> // | hz].
rewrite (@prev_noroot _ a x) //.
by apply: subitvPl hz; rewrite /= (itvP hy).
Qed.

Lemma sgr_neighpl_same p a x :
  {in neighpl p a x &, forall y z, (sgr p.[y] = sgr p.[z])}.
Proof.
by rewrite /neighpl=> y z *; apply: (polyrN0_itv (@prev_noroot p a x)).
Qed.

Lemma neighpr_root p x b : {in neighpr p x b, noroot p}.
Proof. exact: next_noroot. Qed.

Lemma sgr_neighprN p x b :
  p.[x] != 0 -> {in neighpr p x b, forall y, (sgr p.[y] = sgr p.[x])}.
Proof.
rewrite /neighpr=> nrpx /= y hy; symmetry.
apply: (@polyrN0_itv `[x, y]); do ?by rewrite bound_in_itv /= (itvP hy).
move=> z; rewrite (@itv_splitU _ x true) ?itv_xx /=; last first.
  by rewrite bound_in_itv /= (itvP hy).
case/orP=> [|hz]; first by rewrite inE /=; move/eqP->.
rewrite (@next_noroot _ x b) //.
by apply: subitvPr hz; rewrite /= (itvP hy).
Qed.

Lemma sgr_neighpr_same p x b :
  {in neighpr p x b &, forall y z, (sgr p.[y] = sgr p.[z])}.
Proof.
by rewrite /neighpl=> y z *; apply: (polyrN0_itv (@next_noroot p x b)).
Qed.

Lemma uniq_roots a b p : uniq (roots p a b).
Proof.
case p0: (p == 0); first by rewrite (eqP p0) roots0.
by apply: (@sorted_uniq _ <%R); [apply: ltr_trans | apply: ltrr|].
Qed.

Hint Resolve uniq_roots.

Lemma in_roots p (a b x : R) :
  (x \in roots p a b) = [&& root p x, x \in `]a, b[ & p != 0].
Proof.
case: rootsP=> //=; first by rewrite in_nil !andbF.
by move=> p0 hr sr; rewrite andbT -hr andbC.
Qed.

Lemma gdcop_eq0 p q : (gdcop p q == 0) = (q == 0) && (p != 0).
Proof.
case: (eqVneq q 0) => [-> | q0].
  rewrite gdcop0 /= eqxx /=.
  by case: (eqVneq p 0) => [-> | pn0]; rewrite ?(negPf pn0) eqxx ?oner_eq0.
rewrite /gdcop; move: {-1}(size q) (leqnn (size q))=> k hk.
case: (eqVneq p 0) => [-> | p0].
  rewrite eqxx andbF; apply: negPf.
  elim: k q q0 {hk} => [|k ihk] q q0 /=; first by rewrite eqxx oner_eq0.
  case: ifP => _ //.
  by apply: ihk; rewrite gcdp0 divpp ?q0 // polyC_eq0; apply/lc_expn_scalp_neq0.
rewrite p0 (negPf q0) /=; apply: negPf.
elim: k q q0 hk => [|k ihk] /= q q0 hk.
  by move: hk q0; rewrite leqn0 size_poly_eq0; move->.
case: ifP=> cpq; first by rewrite (negPf q0).
apply: ihk.
  rewrite divpN0; last by rewrite gcdp_eq0 negb_and q0.
  by rewrite dvdp_leq // dvdp_gcdl.
rewrite -ltnS; apply: leq_trans hk; move: (dvdp_gcdl q p); rewrite dvdp_eq.
move/eqP=> eqq; move/(f_equal (fun x : {poly R} => size x)): (eqq).
rewrite size_scale; last exact: lc_expn_scalp_neq0.
have gcdn0 : gcdp q p != 0 by rewrite gcdp_eq0 negb_and q0.
have qqn0 : q %/ gcdp q p != 0.
   apply: contraTneq q0; rewrite negbK => e.
   move: (scaler_eq0 (lead_coef (gcdp q p) ^+ scalp q (gcdp q p)) q).
   by rewrite (negPf (lc_expn_scalp_neq0 _ _)) /=; move<-; rewrite eqq e mul0r.
move->; rewrite size_mul //; case sgcd: (size (gcdp q p)) => [|n].
  by move/eqP: sgcd gcdn0; rewrite size_poly_eq0; move->.
case: n sgcd => [|n]; first by move/eqP; rewrite size_poly_eq1 gcdp_eqp1 cpq.
by rewrite addnS /= -{1}[size (_ %/ _)]addn0 ltn_add2l.
Qed.

Lemma roots_mul a b : a < b -> forall p q,
  p != 0 -> q != 0 -> perm_eq (roots (p*q) a b)
  (roots p a b ++ roots ((gdcop p q)) a b).
Proof.
move=> hab p q np0 nq0.
apply: uniq_perm_eq; first exact: uniq_roots.
  rewrite cat_uniq ?uniq_roots andbT /=; apply/hasPn=> x /=.
  move/root_roots; rewrite root_gdco //; case/andP=> _.
  by rewrite in_roots !negb_and=> ->.
move=> x; rewrite mem_cat !in_roots root_gdco //.
rewrite rootM mulf_eq0 gdcop_eq0 negb_and.
case: (x \in `]_, _[); last by rewrite !andbF.
by rewrite negb_or !np0 !nq0 !andbT /=; do 2?case: root=> //=.
Qed.

Lemma roots_mul_coprime a b :
  a < b ->
  forall p q, p != 0 -> q != 0 -> coprimep p q ->
  perm_eq (roots (p * q) a b)
  (roots p a b ++ roots q a b).
Proof.
move=> hab p q np0 nq0 cpq.
rewrite (perm_eq_trans (roots_mul hab np0 nq0)) //.
suff ->: roots (gdcop p q) a b = roots q a b by apply: perm_eq_refl.
case: gdcopP=> r rq hrp; move/(_ q (dvdpp _)).
rewrite coprimep_sym; move/(_ cpq)=> qr.
have erq : r %= q by rewrite /eqp rq qr.
apply/roots_eq=> // [|x hx]; last exact: eqp_root.
by rewrite -size_poly_eq0 (eqp_size erq) size_poly_eq0.
Qed.

Lemma next_rootM a b (p q : {poly R}) :
  next_root (p * q) a b = minr (next_root p a b) (next_root q a b).
Proof.
symmetry; apply: is_next_root.
wlog: p q / next_root p a b <= next_root q a b.
  case: minrP=> hpq; first by move/(_ _ _ hpq); case: minrP hpq.
  by move/(_ _ _ (ltrW hpq)); rewrite mulrC minrC; case: minrP hpq.
case: minrP=> //; case: next_rootP=> [|y np0 py0 hy|c np0 ->] hp hpq _.
* by rewrite hp mul0r root0; constructor.
* rewrite rootM; move/rootP:(py0)->; constructor=> //.
  - by rewrite mulf_neq0 //; case: next_rootP hpq; rewrite // (itvP hy).
  - by rewrite hornerM py0 mul0r.
  - move=> z hz /=; rewrite rootM negb_or ?hp //.
    by rewrite (@next_noroot _ a b) //; apply: subitvPr hz.
* case: (altP (q =P 0))=> q0.
    move: hpq; rewrite q0 mulr0 root0 next_root0 ler_maxl lerr andbT.
    by move=> hba; rewrite maxr_r //; constructor.
  constructor=> //; first by rewrite mulf_neq0.
  move=> z hz /=; rewrite rootM negb_or ?hp //.
  rewrite (@next_noroot _ a b) //; apply: subitvPr hz=> /=.
  by move: hpq; rewrite ler_maxl; case/andP.
Qed.

Lemma neighpr_mul a b p q :
  (neighpr (p * q) a b) =i [predI (neighpr p a b) & (neighpr q a b)].
Proof.
move=> x; rewrite inE /= !inE /= next_rootM.
by case: (a < x); rewrite // ltr_minr.
Qed.

Lemma prev_rootM a b (p q : {poly R}) :
  prev_root (p * q) a b = maxr (prev_root p a b) (prev_root q a b).
Proof.
symmetry; apply: is_prev_root.
wlog: p q / prev_root p a b >= prev_root q a b.
  case: maxrP=> hpq; first by move/(_ _ _ hpq); case: maxrP hpq.
  by move/(_ _ _ (ltrW hpq)); rewrite mulrC maxrC; case: maxrP hpq.
case: maxrP=> //; case: (@prev_rootP p)=> [|y np0 py0 hy|c np0 ->] hp hpq _.
* by rewrite hp mul0r root0; constructor.
* rewrite rootM; move/rootP:(py0)->; constructor=> //.
  - by rewrite mulf_neq0 //; case: prev_rootP hpq; rewrite // (itvP hy).
  - by rewrite hornerM py0 mul0r.
  - move=> z hz /=; rewrite rootM negb_or ?hp //.
    by rewrite (@prev_noroot _ a b) //; apply: subitvPl hz.
* case: (altP (q =P 0))=> q0.
    move: hpq; rewrite q0 mulr0 root0 prev_root0 ler_minr lerr andbT.
    by move=> hba; rewrite minr_r //; constructor.
  constructor=> //; first by rewrite mulf_neq0.
  move=> z hz /=; rewrite rootM negb_or ?hp //.
  rewrite (@prev_noroot _ a b) //; apply: subitvPl hz=> /=.
  by move: hpq; rewrite ler_minr; case/andP.
Qed.

Lemma neighpl_mul a b p q :
  (neighpl (p * q) a b) =i [predI (neighpl p a b) & (neighpl q a b)].
Proof.
move=> x; rewrite !inE /= prev_rootM.
by case: (x < b); rewrite // ltr_maxl !(andbT, andbF).
Qed.

Lemma neighpr_wit p x b : x < b -> p != 0 -> {y | y \in neighpr p x b}.
Proof.
move=> xb; exists (mid x (next_root p x b)).
by rewrite mid_in_itv //= next_root_gt.
Qed.

Lemma neighpl_wit p a x : a < x -> p != 0 -> {y | y \in neighpl p a x}.
Proof.
move=> xb; exists (mid (prev_root p a x) x).
by rewrite mid_in_itv //= prev_root_lt.
Qed.

End NeighborHood.

Section SignRight.

Definition sgp_right (p : {poly R}) x :=
  let fix aux (p : {poly R}) n :=
  if n is n'.+1
    then if ~~ root p x
      then sgr p.[x]
      else aux p^`() n'
    else 0
      in aux p (size p).

Lemma sgp_right0 x : sgp_right 0 x = 0.
Proof. by rewrite /sgp_right size_poly0. Qed.

Lemma sgr_neighpr b p x :
  {in neighpr p x b, forall y, (sgr p.[y] = sgp_right p x)}.
Proof.
elim: (size p) {-2}p (leqnn (size p))=> [|n ihn] {p} p.
  rewrite leqn0 size_poly_eq0 /neighpr; move/eqP=> -> /=.
  by move=> y; rewrite next_root0 itv_xx.
rewrite leq_eqVlt ltnS; case/orP; last exact: ihn.
move/eqP=> sp; rewrite /sgp_right sp /=.
case px0: root=> /=; last first.
  move=> y; rewrite /neighpr => hy /=; symmetry.
  apply: (@polyrN0_itv `[x, y]); do ?by rewrite bound_in_itv /= (itvP hy).
  move=> z; rewrite (@itv_splitU _ x true) ?bound_in_itv /= ?(itvP hy) //.
  rewrite itv_xx /=; case/predU1P=> hz; first by rewrite hz px0.
  rewrite (@next_noroot p x b) //.
  by apply: subitvPr hz=> /=; rewrite (itvP hy).
have <-: size p^`() = n by rewrite size_deriv sp.
rewrite -/(sgp_right p^`() x).
move=> y; rewrite /neighpr=> hy /=.
case: (@neighpr_wit (p * p^`()) x b)=> [||m hm].
* case: next_rootP hy; first by rewrite itv_xx.
    by move=> ? ? ?; move/itvP->.
  by move=> c p0 -> _; case: maxrP=> _; rewrite ?itv_xx //; move/itvP->.
* rewrite mulf_neq0 //.
    by move/eqP:sp; apply: contraTneq=> ->; rewrite size_poly0.
  move: (size_deriv p); rewrite sp /=; move/eqP; apply: contraTneq=> ->.
  rewrite size_poly0; apply: contraTneq px0=> hn; rewrite -hn in sp.
  by move/eqP: sp; case/size_poly1P=> c nc0 ->; rewrite rootC.
* move: hm; rewrite neighpr_mul /neighpr inE /=; case/andP=> hmp hmp'.
  rewrite (polyrN0_itv _ hmp) //; last exact: next_noroot.
  rewrite (@ders0r p x m (mid x m)) ?(eqP px0) ?mid_in_itv ?bound_in_itv //;
    rewrite /= ?(itvP hmp) //; last first.
    move=> u hu /=; rewrite (@next_noroot _ x b) //.
    by apply: subitvPr hu; rewrite /= (itvP hmp').
  rewrite ihn ?size_deriv ?sp /neighpr //.
  by rewrite (subitvP _ (@mid_in_itv _ true true _ _ _)) //= ?lerr (itvP hmp').
Qed.

Lemma sgr_neighpl a p x :
  {in neighpl p a x, forall y,
    (sgr p.[y] = (-1) ^+ (odd (\mu_x p)) * sgp_right p x)
  }.
Proof.
elim: (size p) {-2}p (leqnn (size p))=> [|n ihn] {p} p.
  rewrite leqn0 size_poly_eq0 /neighpl; move/eqP=> -> /=.
  by move=> y; rewrite prev_root0 itv_xx.
rewrite leq_eqVlt ltnS; case/orP; last exact: ihn.
move/eqP=> sp; rewrite /sgp_right sp /=.
case px0: root=> /=; last first.
  move=> y; rewrite /neighpl => hy /=; symmetry.
  move: (negbT px0); rewrite -mu_gt0; last first.
    by apply: contraFN px0; move/eqP->; rewrite rootC.
  rewrite -leqNgt leqn0; move/eqP=> -> /=; rewrite expr0 mul1r.
  symmetry; apply: (@polyrN0_itv `[y, x]);
    do ?by rewrite bound_in_itv /= (itvP hy).
  move=> z; rewrite (@itv_splitU _ x false) ?bound_in_itv /= ?(itvP hy) //.
  rewrite itv_xx /= orbC; case/predU1P=> hz; first by rewrite hz px0.
  rewrite (@prev_noroot p a x) //.
  by apply: subitvPl hz=> /=; rewrite (itvP hy).
have <-: size p^`() = n by rewrite size_deriv sp.
rewrite -/(sgp_right p^`() x).
move=> y; rewrite /neighpl=> hy /=.
case: (@neighpl_wit (p * p^`()) a x)=> [||m hm].
* case: prev_rootP hy; first by rewrite itv_xx.
    by move=> ? ? ?; move/itvP->.
  by move=> c p0 -> _; case: minrP=> _; rewrite ?itv_xx //; move/itvP->.
* rewrite mulf_neq0 //.
    by move/eqP:sp; apply: contraTneq=> ->; rewrite size_poly0.
  move: (size_deriv p); rewrite sp /=; move/eqP; apply: contraTneq=> ->.
  rewrite size_poly0; apply: contraTneq px0=> hn; rewrite -hn in sp.
  by move/eqP: sp; case/size_poly1P=> c nc0 ->; rewrite rootC.
* move: hm; rewrite neighpl_mul /neighpl inE /=; case/andP=> hmp hmp'.
  rewrite (polyrN0_itv _ hmp) //; last exact: prev_noroot.
  rewrite (@ders0l p m x (mid m x)) ?(eqP px0) ?mid_in_itv ?bound_in_itv //;
    rewrite /= ?(itvP hmp) //; last first.
    move=> u hu /=; rewrite (@prev_noroot _ a x) //.
    by apply: subitvPl hu; rewrite /= (itvP hmp').
  rewrite ihn ?size_deriv ?sp /neighpl //; last first.
    by rewrite (subitvP _ (@mid_in_itv _ true true _ _ _)) //=
       ?lerr (itvP hmp').
  rewrite mu_deriv // odd_sub ?mu_gt0 //=; last by rewrite -size_poly_eq0 sp.
  by rewrite signr_addb /= mulrN1 mulNr opprK.
Qed.

Lemma sgp_right_deriv (p : {poly R}) x :
  root p x -> sgp_right p x = sgp_right (p^`()) x.
Proof.
elim: (size p) {-2}p (erefl (size p)) x => {p} [p|sp hp p hsp x].
  by move/eqP; rewrite size_poly_eq0; move/eqP=> -> x _; rewrite derivC.
by rewrite /sgp_right size_deriv hsp /= => ->.
Qed.

Lemma sgp_rightNroot (p : {poly R}) x :
  ~~ root p x -> sgp_right p x = sgr p.[x].
Proof.
move=> nrpx; rewrite /sgp_right; case hsp: (size _)=> [|sp].
  by move/eqP:hsp; rewrite size_poly_eq0; move/eqP->; rewrite hornerC sgr0.
by rewrite nrpx.
Qed.

Lemma sgp_right_mul p q x : sgp_right (p * q) x = sgp_right p x * sgp_right q x.
Proof.
case: (altP (q =P 0))=> q0; first by rewrite q0 /sgp_right !(size_poly0,mulr0).
case: (altP (p =P 0))=> p0; first by rewrite p0 /sgp_right !(size_poly0,mul0r).
case: (@neighpr_wit (p * q) x (1 + x))=> [||m hpq]; do ?by rewrite mulf_neq0.
  by rewrite ltr_spaddl ?ltr01.
rewrite -(@sgr_neighpr (1 + x) _ _ m) //.
move: hpq; rewrite neighpr_mul inE /=; case/andP=> hp hq.
by rewrite hornerM sgrM !(@sgr_neighpr (1 + x) _ x) /neighpr.
Qed.

Lemma sgp_right_scale c p x : sgp_right (c *: p) x = sgr c * sgp_right p x.
Proof.
case c0: (c == 0); first by rewrite (eqP c0) scale0r sgr0 mul0r sgp_right0.
by rewrite -mul_polyC sgp_right_mul sgp_rightNroot ?hornerC ?rootC ?c0.
Qed.

Lemma sgp_right_square p x : p != 0 -> sgp_right p x * sgp_right p x = 1.
Proof.
move=> np0; case: (@neighpr_wit p x (1 + x))=> [||m hpq] //.
  by rewrite ltr_spaddl ?ltr01.
rewrite -(@sgr_neighpr (1 + x) _ _ m) //.
by rewrite -expr2 sqr_sg (@next_noroot _ x (1 + x)).
Qed.

Lemma sgp_right_rec p x :
  sgp_right p x =
   (if p == 0 then 0 else if ~~ root p x then sgr p.[x] else sgp_right p^`() x).
Proof.
rewrite /sgp_right; case hs: size => [|s]; rewrite -size_poly_eq0 hs //=.
by rewrite size_deriv hs.
Qed.

Lemma sgp_right_addp0 (p q : {poly R}) x :
  q != 0 -> (\mu_x p > \mu_x q)%N -> sgp_right (p + q) x = sgp_right q x.
Proof.
move=> nq0; move hm: (\mu_x q)=> m.
elim: m p q nq0 hm => [|mq ihmq] p q nq0 hmq; case hmp: (\mu_x p)=> // [mp];
  do[
    rewrite ltnS=> hm;
      rewrite sgp_right_rec {1}addrC;
        rewrite GRing.Theory.addr_eq0].   case: (altP (_ =P _))=> hqp.
    move: (nq0); rewrite {1}hqp oppr_eq0=> np0.
    rewrite sgp_right_rec (negPf nq0) -mu_gt0 // hmq /=.
    apply/eqP; rewrite eq_sym hqp hornerN sgrN.
    by rewrite oppr_eq0 sgr_eq0 -[_ == _]mu_gt0 ?hmp.
  rewrite rootE hornerD.
  have ->: p.[x] = 0.
    apply/eqP; rewrite -[_ == _]mu_gt0 ?hmp //.
    by move/eqP: hmp; apply: contraTneq=> ->; rewrite mu0.
  symmetry; rewrite sgp_right_rec (negPf nq0) add0r.
  by rewrite -/(root _ _) -mu_gt0 // hmq.
case: (altP (_ =P _))=> hqp.
  by move: hm; rewrite -ltnS -hmq -hmp hqp mu_opp ltnn.
have px0: p.[x] = 0.
  apply/rootP; rewrite -mu_gt0 ?hmp //.
  by move/eqP: hmp; apply: contraTneq=> ->; rewrite mu0.
have qx0: q.[x] = 0 by apply/rootP; rewrite -mu_gt0 ?hmq //.
rewrite rootE hornerD px0 qx0 add0r eqxx /=; symmetry.
rewrite sgp_right_rec rootE (negPf nq0) qx0 eqxx /=.
rewrite derivD ihmq // ?mu_deriv ?rootE ?px0 ?qx0 ?hmp ?hmq ?subn1 //.
apply: contra nq0; rewrite -size_poly_eq0 size_deriv.
case hsq: size=> [|sq] /=.
  by move/eqP: hsq; rewrite size_poly_eq0.
move/eqP=> sq0; move/eqP: hsq qx0; rewrite sq0; case/size_poly1P=> c c0 ->.
by rewrite hornerC; move/eqP; rewrite (negPf c0).
Qed.

End SignRight.

Section PolyRCFPdiv.
Import Pdiv.Ring Pdiv.ComRing.

Lemma sgp_rightc (x c : R) : sgp_right c%:P x = sgr c.
Proof.
rewrite /sgp_right size_polyC.
case cn0: (_ == 0)=> /=; first by rewrite (eqP cn0) sgr0.
by rewrite rootC hornerC cn0.
Qed.

Lemma sgp_right_eq0 (x : R) p : (sgp_right p x == 0) = (p == 0).
Proof.
case: (altP (p =P 0))=> p0; first by rewrite p0 sgp_rightc sgr0 eqxx.
rewrite /sgp_right.
elim: (size p) {-2}p (erefl (size p)) p0=> {p} [|sp ihsp] p esp p0.
  by move/eqP:esp; rewrite size_poly_eq0 (negPf p0).
rewrite esp /=; case px0: root=> //=; rewrite ?sgr_cp0 ?px0//.
have hsp: sp = size p^`() by rewrite size_deriv esp.
rewrite hsp ihsp // -size_poly_eq0 -hsp; apply/negP; move/eqP=> sp0.
move: px0; rewrite root_factor_theorem.
by move=> /rdvdp_leq // /(_ p0); rewrite size_XsubC esp sp0.
Qed.

Lemma lc_expn_rscalp_neq0 (p q : {poly R}): lead_coef q ^+ rscalp p q != 0.
Proof.
case: (eqVneq q 0) => [->|nzq]; last by rewrite expf_neq0 ?lead_coef_eq0.
by rewrite /rscalp unlock /= eqxx /= expr0 oner_neq0.
Qed.
Notation lcn_neq0 := lc_expn_rscalp_neq0.

Lemma sgp_right_mod p q x : (\mu_x p < \mu_x q)%N ->
  sgp_right (rmodp p q) x = (sgr (lead_coef q)) ^+ (rscalp p q) * sgp_right p x.
Proof.
move=> mupq; case p0: (p == 0).
  by rewrite (eqP p0) rmod0p !sgp_right0 mulr0.
have qn0 : q != 0.
  by apply/negP; move/eqP=> q0; rewrite q0 mu0 ltn0 in mupq.
move/eqP: (rdivp_eq q p).
rewrite eq_sym (can2_eq (addKr _ ) (addNKr _)); move/eqP->.
case qpq0: ((rdivp p q) == 0).
  by rewrite (eqP qpq0) mul0r oppr0 add0r sgp_right_scale // sgrX.
rewrite sgp_right_addp0 ?sgp_right_scale ?sgrX //.
  by rewrite scaler_eq0 negb_or p0 lcn_neq0.
rewrite mu_mulC ?lcn_neq0 // mu_opp mu_mul ?mulf_neq0 ?qpq0 //.
by rewrite ltn_addl.
Qed.

Lemma rootsC (a b c : R) : roots c%:P a b = [::].
Proof.
case: (altP (c =P 0))=> hc; first by rewrite hc roots0.
by apply: no_root_roots=> x hx; rewrite rootC.
Qed.

Lemma rootsZ a b c p : c != 0 -> roots (c *: p) a b = roots p a b.
Proof.
have [->|p_neq0 c_neq0] := eqVneq p 0; first by rewrite scaler0.
by apply/roots_eq => [||x axb]; rewrite ?scaler_eq0 ?(negPf c_neq0) ?rootZ.
Qed.

Lemma root_bigrgcd (x : R) (ps : seq {poly R}) :
  root (\big[(@rgcdp _)/0]_(p <- ps) p) x = all (root^~ x) ps.
Proof.
elim: ps; first by rewrite big_nil root0.
move=> p ps ihp; rewrite big_cons /=.
by rewrite (eqp_root (eqp_rgcd_gcd _ _)) root_gcd ihp.
Qed.

Definition rootsR p := roots p (- cauchy_bound p) (cauchy_bound p).

Lemma roots_on_rootsR p : p != 0 -> roots_on p `]-oo, +oo[ (rootsR p).
Proof.
rewrite /rootsR => p_neq0 x /=; rewrite -roots_on_roots // andbC.
by have [/(cauchy_boundP p_neq0) /=|//] := altP rootP; rewrite ltr_norml.
Qed.

Lemma rootsR0 : rootsR 0 = [::]. Proof. exact: roots0. Qed.

Lemma rootsRC c : rootsR c%:P = [::]. Proof. exact: rootsC. Qed.

Lemma rootsRP p a b :
    {in `]-oo, a], noroot p} -> {in `[b , +oo[, noroot p} ->
  roots p a b = rootsR p.
Proof.
move=> rpa rpb.
have [->|p_neq0] := eqVneq p 0; first by rewrite rootsR0 roots0.
apply: (eq_sorted_irr (@ltr_trans _)); rewrite ?sorted_roots // => x.
rewrite -roots_on_rootsR -?roots_on_roots //=.
have [rpx|] := boolP (root _ _); rewrite ?(andbT, andbF) //.
apply: contraLR rpx; rewrite inE negb_and -!lerNgt.
by move=> /orP[/rpa //|xb]; rewrite rpb // inE andbT.
Qed.

Lemma sgp_pinftyP x (p : {poly R}) :
    {in `[x , +oo[, noroot p} ->
  {in `[x, +oo[, forall y, sgr p.[y] = sgp_pinfty p}.
Proof.
rewrite /sgp_pinfty; wlog lp_gt0 : x p / lead_coef p > 0 => [hwlog|rpx y Hy].
  have [|/(hwlog x p) //|/eqP] := ltrgtP (lead_coef p) 0; last first.
    by rewrite lead_coef_eq0 => /eqP -> ? ? ?; rewrite lead_coef0 horner0.
  rewrite -[p]opprK lead_coef_opp oppr_cp0 => /(hwlog x _) Hp HNp y Hy.
  by rewrite hornerN !sgrN Hp => // z /HNp; rewrite rootN.
have [z Hz] := poly_pinfty_gt_lc lp_gt0.
have {Hz} Hz u : u \in `[z, +oo[ -> Num.sg p.[u] = 1.
  by rewrite inE andbT => /Hz pu_ge1; rewrite gtr0_sg // (ltr_le_trans lp_gt0).
rewrite (@polyrN0_itv _ _ rpx (maxr y z)) ?inE ?ler_maxr ?(itvP Hy) //.
by rewrite Hz ?gtr0_sg // inE ler_maxr lerr orbT.
Qed.

Lemma sgp_minftyP x (p : {poly R}) :
    {in `]-oo, x], noroot p} ->
  {in `]-oo, x], forall y, sgr p.[y] = sgp_minfty p}.
Proof.
move=> rpx y Hy; rewrite -sgp_pinfty_sym.
have -> : p.[y] = (p \Po -'X).[-y] by rewrite horner_comp !hornerE opprK.
apply: (@sgp_pinftyP (- x)); last by rewrite inE ler_opp2 (itvP Hy).
by move=> z Hz /=; rewrite root_comp !hornerE rpx // inE ler_oppl (itvP Hz).
Qed.

Lemma odd_poly_root (p : {poly R}) : ~~ odd (size p) -> {x | root p x}.
Proof.
move=> size_p_even.
have [->|p_neq0] := altP (p =P 0); first by exists 0; rewrite root0.
pose b := cauchy_bound p.
have [] := @ivt_sign p (-b) b; last by move=> x _; exists x.
  by rewrite ge0_cp // ?cauchy_bound_ge0.
rewrite (sgp_minftyP (le_cauchy_bound p_neq0)) ?bound_in_itv //.
rewrite (sgp_pinftyP (ge_cauchy_bound p_neq0)) ?bound_in_itv //.
move: size_p_even; rewrite polySpred //= negbK /sgp_minfty -signr_odd => ->.
by rewrite expr1 mulN1r sgrN mulNr -expr2 sqr_sg lead_coef_eq0 p_neq0.
Qed.
End PolyRCFPdiv.

End PolyRCF.