(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
Require Import bigop ssralg poly polydiv ssrnum zmodp.
Require Import polyorder path interval ssrint.

(****************************************************************************)
(* This files contains basic (and unformatted) theory for polynomials       *)
(* over a realclosed fields. From the IVT (contained in the rcfType         *)
(* structure), we derive Rolle's Theorem, the Mean Value Theorem, a root    *)
(* isolation procedure and the notion of neighborhood.                      *)
(*                                                                          *)
(*    sgp_minfty p == the sign of p in -oo                                  *)
(*    sgp_pinfty p == the sign of p in +oo                                  *)
(*  cauchy_bound p == the cauchy bound of p                                 *)
(*                    (this strictly bounds the norm of roots of p)         *)
(*     roots p a b == the ordered list of roots of p in  `[a, b]            *)
(*                    defaults to [::] when p == 0                          *)
(*        rootsR p == the ordered list of all roots of p, ([::] if p == 0). *)
(* next_root p x b == the smallest root of p contained in `[x, maxn x b]    *)
(*                    if p has no root on `[x, maxn x b], we pick maxn x b. *)
(* prev_root p x a == the smallest root of p contained in `[minn x a, x]    *)
(*                    if p has no root on `[minn x a, x], we pick minn x a. *)
(*   neighpr p a b := `]a, next_root p a b[.                                *)
(*                 == an open interval of the form `]a, x[, with x <= b     *)
(*                    in which p has no root.                               *)
(*   neighpl p a b := `]prev_root p a b, b[.                                *)
(*                 == an open interval of the form `]x, b[, with a <= x     *)
(*                    in which p has no root.                               *)
(*   sgp_right p a == the sign of p on the right of a.                      *)
(****************************************************************************)


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 : forall (R : ringType) (s: seq R) (c:R), c != 0 ->
  (last c s != 0) = (last 1 s != 0).
Proof. by move=> R'; elim=> [|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.

(******************************************************************)
(* Definitions and properties for polynomials in a numDomainType. *)
(******************************************************************)
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.

(******************************************************************)
(* Definitions and properties for polynomials in a realFieldType. *)
(******************************************************************)
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.

(* :REMARK: not necessary here ! *)
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|.

(* Could be a sharp bound, and proof should shrink... *)
Lemma cauchy_boundP : forall (p : {poly R}) x,
  p != 0 -> p.[x] = 0 -> `| x | < cauchy_bound p.
Proof.
move=> p x 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 // big_distrl /=.
rewrite 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.
(* this could be improved a little bit with int exponents *)
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.

(************************************************************)
(* Definitions and properties for polynomials in a rcfType. *)
(************************************************************)
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}.

(* we restate poly_ivt in a nicer way. Perhaps the def of PolyRCF should *)
(* be moved in this file, juste above this section                       *)

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; exact/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 : forall (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=> a P 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) [_ %% _]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.

(* Todo : orderedpoly !! *)
(* Lemma deriv_expz_nat : forall (n : nat) p, (p ^ n)^`() = (p^`() * p ^ (n.-1)) *~ n. *)
(* Proof. *)
(* elim=> [|n ihn] p /=; first by rewrite expr0z derivC mul0zr. *)
(* rewrite exprSz_nat derivM ihn mulzrAr mulrCA -exprSz_nat. *)
(* by case: n {ihn}=> [|n] //; rewrite mul0zr addr0 mul1zr. *)
(* Qed. *)

(* Definition derivCE := (derivE, deriv_expz_nat). *)

(* Lemma size_poly_ind : forall K : {poly R} -> Prop, *)
(*   K 0 ->  *)
(*   (forall p sp, size p = sp.+1 ->   *)
(*     forall q, (size q <= sp)%N -> K q -> K p) *)
(*   -> forall p, K p. *)
(* Proof. *)
(* move=> K K0 ihK p. *)
(* move: {-2}p (leqnn (size p)); elim: (size p)=> {p} [|n ihn] p spn. *)
(*   by move: spn; rewrite leqn0 size_poly_eq0; move/eqP->. *)
(* case spSn: (size p == n.+1). *)
(*   move/eqP:spSn; move/ihK=> ihKp; apply: (ihKp 0)=>//. *)
(*   by rewrite size_poly0. *)
(* by move:spn; rewrite leq_eqVlt spSn /= ltnS; by move/ihn.  *)
(* Qed. *)

(* Lemma size_poly_indW : forall K : {poly R} -> Prop, *)
(*   K 0 ->  *)
(*   (forall p sp, size p = sp.+1 ->   *)
(*     forall q, size q = sp -> K q -> K p) *)
(*   -> forall p, K p. *)
(* Proof. *)
(* move=> K K0 ihK p. *)
(* move: {-2}p (leqnn (size p)); elim: (size p)=> {p} [|n ihn] p spn. *)
(*   by move: spn; rewrite leqn0 size_poly_eq0; move/eqP->. *)
(* case spSn: (size p == n.+1). *)
(*   move/eqP:spSn; move/ihK=> ihKp; case: n ihn spn ihKp=> [|n] ihn spn ihKp. *)
(*     by apply: (ihKp 0)=>//; rewrite size_poly0. *)
(*   apply: (ihKp 'X^n)=>//; first by rewrite size_polyXn. *)
(*   by apply: ihn; rewrite size_polyXn. *)
(* by move:spn; rewrite leq_eqVlt spSn /= ltnS; by move/ihn.  *)
(* Qed. *)

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

Lemma ivt_sign : forall (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=> p a b 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=> //.
(* need for a lemma reditvP *)
rewrite inE /= !ltr_neqAle andbCA -!andbA [_ && (_ <= _)]hc andbT 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 : forall a b p, a < b ->
  p.[a] = 0 -> p.[b] = 0 ->
   {c | (c \in `]a, b[) & (p^`().[c] == 0) || (p.[c] == 0)}.
Proof.
move=> a b p 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 : forall a b p, a < b ->
  p.[a] = p.[b] -> {c | c \in `]a, b[ & p^`().[c] = 0}.
Proof.
move=> a b p 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 : forall a b p, a < b ->
  {c | c \in `]a, b[ & p.[b] - p.[a] = p^`().[c] * (b - a)}.
Proof.
move=> a b p 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 : forall 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=> a b p 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.

(* Section der_root_sg. *)

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

(* Lemma derp_root : a <= b -> sgr p.[a] != sgr 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 hs : sgr p.[a] * sgr p.[b] == -1. *)
(*   by rewrite -sgrM sgr_cp0 mulr_lt0_gt0 ?(itvP hpab). *)
(* case: (ivt_sign ivt 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 : forall p i s, roots_on p i s -> {in i, root p =1 mem s}.
Proof. by move=> p i s hp x hx; move: (hp x); rewrite hx. Qed.

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

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

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

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

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

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

End RootsOn.


(* (* Symmetry of center a *) *)
(* Definition symr (a x : R) := a - x. *)

(* Lemma symr_inv : forall a, involutive (symr a). *)
(* Proof. by move=> a y; rewrite /symr opprD addrA subrr opprK add0r. Qed. *)

(* Lemma symr_inj : forall a, injective (symr a). *)
(* Proof. by move=> a; apply: inv_inj; apply: symr_inv. Qed. *)

(* Lemma ltr_sym : forall a x y, (symr a x < symr a y) = (y < x). *)
(* Proof. by move=> a x y; rewrite lter_add2r lter_oppr opprK. Qed. *)

(* Lemma symr_add_itv : forall a b x,  *)
(*   (a < symr (a + b) x < b) = (a < x < b). *)
(* Proof.  *)
(* move=> a b x; rewrite andbC.    *)
(* by rewrite lter_subrA lter_add2r -lter_addlA lter_add2l. *)
(* Qed. *)

Lemma roots_on_comp : forall p a b s,
  roots_on (p \Po (-'X)) `](-b), (-a)[
  (map (-%R) s) <-> roots_on p `]a, b[ s.
Proof.
move=> p a b /= s; 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 : forall 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=> p a b x s 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 : forall 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=> p a b x s; move/allP=> lsx; move/roots_on_comp=> /=.
move/min_roots_on; case.
  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 : forall p a b r s,
  sorted <%R (r :: s) -> roots_on p `]a, b[ (r :: s) -> roots_on p `]r, b[ s.
Proof.
move=> p a b r s /= hrs hr.
have:= (order_path_min (@ltr_trans _) hrs)=> allrs.
by case: (min_roots_on allrs hr).
Qed.
(* move=> p a b r s hp hr x; apply/andP/idP. *)
(*   have:= (order_path_min (@ltr_trans _) hp) => /=; case/andP=> ar1 _. *)
(*   case; move/ooitvP=> rxb rpx; move: (hr x); rewrite in_cons rpx andbT. *)
(*   by rewrite rxb andbT (ltr_trans ar1) 1?eq_sym ?ltr_eqF  ?rxb. *)
(* move=> spx. *)
(* have xrsp: x \in r :: s by rewrite in_cons spx orbT. *)
(* rewrite (roots_on_root hr) //. *)
(* rewrite (roots_on_in hr xrsp); move: hp => /=; case/andP=> _. *)
(* by move/(order_path_min (@ltr_trans _)); move/allP; move/(_ _ spx)->. *)
(* 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.


(* move=> p a b r s; rewrite -{1}[s]revK -!rev_cons rev_sorted. *)
(* rewrite  [r :: _]lock /=; unlock; move=> hp hr x; apply/andP/idP. *)
(*   have:= (order_path_min (rev_trans (@ltr_trans _)) hp) => /=. *)
(*   case/andP=> ar1 _; case; move/ooitvP=> axr rpx. *)
(*   move: (hr x); rewrite mem_rcons in_cons rpx andbT axr andTb. *)
(*   by rewrite ((rev_trans (@ltr_trans _) ar1)) ?ltr_eqF ?axr. *)
(* move=> spx. *)
(* have xrsp: x \in rcons s r by rewrite mem_rcons in_cons spx orbT. *)
(* rewrite (roots_on_root hr) //. *)
(* rewrite (roots_on_in hr xrsp); move: hp => /=; case/andP=> _. *)
(* move/(order_path_min (rev_trans (@ltr_trans _))); move/allP.  *)
(* by move/(_ x)=> -> //; rewrite mem_rev. *)
(* Qed. *)

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

Lemma monotonic_rootN :  forall (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=> p a b 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.

(* Inductive polN0 : Type := PolN0 : forall p : {poly R}, p != 0 -> polN0. *)

(* Coercion pol_of_polN0 i := let: PolN0 p _ := i in p. *)

(* Canonical Structure polN0_subType := [subType for pol_of_polN0]. *)
(* Definition polN0_eqMixin := Eval hnf in [eqMixin of polN0 by <:]. *)
(* Canonical Structure polN0_eqType := *)
(*   Eval hnf in EqType polN0 polN0_eqMixin. *)
(* Definition polN0_choiceMixin := [choiceMixin of polN0 by <:]. *)
(* Canonical Structure polN0_choiceType := *)
(*   Eval hnf in ChoiceType polN0 polN0_choiceMixin. *)

(* Todo : Lemmas about operations of intervall :
   itversection, restriction and splitting *)
Lemma cat_roots_on : forall (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=> p a b x 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.

(* still much too long *)
Lemma itv_roots : forall (p :{poly R}) (a b : R),
  {s : seq R & roots_spec p (topred `]a, b[) s p (p == 0) s}.
Proof.
move=> p a b; 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 : forall p a b,
  roots_spec p (topred `]a, b[) (roots p a b) p (p == 0) (roots p a b).
Proof. by move=> p a b; rewrite /roots; case hp: itv_roots. Qed.

Lemma roots0 : forall a b, roots 0 a b = [::].
Proof. by move=> a b; 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 : forall a b p, sorted <%R (roots p a b).
Proof. by move=> p a b; case: rootsP. Qed.
Hint Resolve sorted_roots.

Lemma path_roots : forall p a b, path <%R a (roots p a b).
Proof.
move=> p a b; 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 :
   forall (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 move=> p a b; case: rootsP=> // p0 hs ps _ y hy /=; rewrite -hs hy.
Qed.

Lemma root_in_roots : forall (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=> p a b p0 x axb rpx; rewrite -root_is_roots. Qed.

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

Lemma roots_nil : forall p a b, p != 0 ->
  roots p a b = [::] -> {in `]a, b[, noroot p}.
Proof.
move=> p a b; 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 *; exact: (roots_on_in ron_p). Qed.

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

Lemma roots_on_uniq : forall 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.
move=> p a b s1.
elim: s1 p a b => [| 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 : forall (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=> p q a b 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 : forall p, roots (- p) =2 roots p.
Proof.
move=> p 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 : forall (p : {poly R}) a b,
  {in `]a, b[ , noroot p} -> roots p a b = [::].
Proof.
move=> p a b 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 : forall p a b s, a < b ->
  roots_on p `]a, b[ s -> a < head b s.
Proof.
move=> p a b [|x s] ab //; move/(_ 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 : forall p a b s, a < b ->
  roots_on p `]a, b[ s -> last a s < b.
Proof.
move=> p a b [|x s] ab rs //.
by rewrite (itvP (roots_on_in rs _)) //= mem_last.
Qed.

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

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

Lemma roots_cons : forall 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.
move=> p a b x s; 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 : forall 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.
move=> p a b x s; 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 : forall a b, next_root 0 a b = a.
Proof. by move=> *; 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 : forall (p : {poly R}) a b, next_root_spec p a b (p.[next_root p a b] == 0) (next_root p a b).
Proof.
move=> p a b; 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 : forall p a b, next_root p a b \in `[a, maxr b a].
Proof.
move=> p a b; 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 : forall p a b, a < b -> p != 0 -> next_root p a b > a.
Proof.
move=> p a b 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 : forall p a b, {in `]a, (next_root p a b)[, noroot p}.
Proof.
move=> p a b 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 : forall p a b x, next_root_spec p a b (root p x) x -> x = next_root p a b.
Proof.
move=> p a b x []; 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 : forall a b, prev_root 0 a b = b.
Proof. by move=> *; 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 : forall (p : {poly R}) a b, prev_root_spec p a b (p.[prev_root p a b] == 0) (prev_root p a b).
Proof.
move=> p a b; 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 : forall p a b, prev_root p a b \in `[minr a b, b].
Proof.
move=> p a b; 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 : forall p a b, {in `](prev_root p a b), b[, noroot p}.
Proof.
move=> p a b 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 : forall p a b, a < b -> p != 0 -> prev_root p a b < b.
Proof.
move=> p a b 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 : forall p a b x, prev_root_spec p a b (root p x) x -> x = prev_root p a b.
Proof.
move=> p a b x []; 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 : forall p a x,  {in neighpl p a x, noroot p}.
Proof. exact: prev_noroot. Qed.

Lemma sgr_neighplN : forall p a x, ~~root p x ->
  {in neighpl p a x, forall y, (sgr p.[y] = sgr p.[x])}.
Proof.
rewrite /neighpl=> p a x 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.
(* Todo : Lemma itv_splitP *)
  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 : forall p a x,
  {in neighpl p a x &, forall y z, (sgr p.[y] = sgr p.[z])}.
Proof.
by rewrite /neighpl=> p x b y z *; apply: (polyrN0_itv (@prev_noroot p x b)).
Qed.

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

Lemma sgr_neighprN : forall p x b, p.[x] != 0 ->
  {in neighpr p x b, forall y, (sgr p.[y] = sgr p.[x])}.
Proof.
rewrite /neighpr=> p x b 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.
(* Todo : Lemma itv_splitP *)
  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 : forall p x b,
  {in neighpr p x b &, forall y z, (sgr p.[y] = sgr p.[z])}.
Proof.
by rewrite /neighpl=> p x b y z *; apply: (polyrN0_itv (@next_noroot p x b)).
Qed.

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

Hint Resolve uniq_roots.

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

(* Todo : move to polyorder => need char 0 *)
Lemma gdcop_eq0 : forall p q, (gdcop p q == 0) = (q == 0) && (p != 0).
Proof.
move=> p q; 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=> _ //.
  apply: ihk; rewrite gcdp0 divpp  ?q0 // polyC_eq0; exact: 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 : forall 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=> a b 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 : forall 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=> a b 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.
(* Todo : relate eqp with roots *)
apply/roots_eq=> // [|x hx]; last exact: eqp_root.
by rewrite -size_poly_eq0 (eqp_size erq) size_poly_eq0.
Qed.


Lemma next_rootM : forall a b (p q : {poly R}),
  next_root (p * q) a b = minr (next_root p a b) (next_root q a b).
Proof.
move=> a b p q; 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 : forall a b p q,
  (neighpr (p * q) a b) =i [predI (neighpr p a b) & (neighpr q a b)].
Proof.
move=> a b p q x; rewrite inE /= !inE /= next_rootM.
by case: (a < x); rewrite // ltr_minr.
Qed.

Lemma prev_rootM : forall a b (p q : {poly R}),
  prev_root (p * q) a b = maxr (prev_root p a b) (prev_root q a b).
Proof.
move=> a b p q; 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 : forall a b p q,
  (neighpl (p * q) a b) =i [predI (neighpl p a b) & (neighpl q a b)].
Proof.
move=> a b p q x; rewrite !inE /= prev_rootM.
by case: (x < b); rewrite // ltr_maxl !(andbT, andbF).
Qed.

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

Lemma neighpl_wit : forall p a x, a < x -> p != 0 -> {y | y \in neighpl p a x}.
Proof.
move=> p a x 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 : forall x, sgp_right 0 x = 0.
Proof. by move=> x; rewrite /sgp_right size_poly0. Qed.

Lemma sgr_neighpr : forall b p x,
  {in neighpr p x b, forall y, (sgr p.[y] = sgp_right p x)}.
Proof.
move=> b p x.
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.
  (* Todo : a lemma for this *)
  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 : forall a p x,
  {in neighpl p a x, forall y,
    (sgr p.[y] = (-1) ^+ (odd (\mu_x p)) * sgp_right p x)
  }.
Proof.
move=> a p x.
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.
  (* Todo : a lemma for this *)
  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 : forall (p : {poly R}) x, root p x ->
  sgp_right p x = sgp_right (p^`()) x.
Proof.
move=> p; elim: (size p) {-2}p (erefl (size p)) => {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 : forall (p : {poly R}) x,
  ~~ root p x -> sgp_right p x = sgr p.[x].
Proof.
move=> p x 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 : forall p q x,
  sgp_right (p * q) x = sgp_right p x * sgp_right q x.
Proof.
move=> p q x.
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 : forall p x, p != 0 -> sgp_right p x * sgp_right p x = 1.
Proof.
move=> p x 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 : forall (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=> p q x 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]. (* Todo : fix this ! *)
  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.

(* redistribute some of what follows with in the file *)
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.

(* :TODO: backport to polydiv *)
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 : forall 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=> p q x 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.