proposition: Lemma one_root1_unique : forall q a b, one_root1 q a b -> unique_root_for (horner q) a b.
proof: Proof. move=> q a b [c [d [k [itv]]]]. rewrite /pos_in_interval /neg_in_interval1 /slope_bounded2. move=> itv1 itv2 sl. case/andP: itv=> ac; case/andP=> cd; case/andP=> db k0. have qd0 : q.[d] <= 0. have : (0 <= (-q).[d]). by apply: (poly_border db) => x xitv; rewrite hornerN lter_oppE itv2. by rewrite hornerN lter_oppE. have qc0 : 0 <= q.[c] by apply/ltW/itv1; rewrite ac lexx. have qcd0 : (-q).[c] <= 0 <= (-q).[d] by rewrite !hornerN !lter_oppE qd0 qc0. have [x xin] := (poly_ivt (ltW cd) qcd0). rewrite /root hornerN oppr_eq0 =>/eqP => xr. exists x; split. - by case/andP: xin=> cx xd; rewrite (lt_le_trans ac cx) (le_lt_trans xd db). - by []. - move=> u; case/andP=> au ub qu0. case cu : (u <= c). have : a < u <= c by rewrite cu au. by move/itv1; rewrite qu0 ltxx. case ud : (d < u). have : d < u < b by rewrite ud ub. by move/itv2; rewrite qu0 ltxx. have cu' : c <= u. by apply: ltW; rewrite ltNge cu. have ud' : u <= d. by rewrite leNgt ud. case/andP: xin=> cx xd. case ux : (u <= x). have := (sl _ _ cu' ux xd). rewrite qu0 xr subrr -(mulr0 k) ler_pmul2l // subr_le0 => xu. by apply/eqP; rewrite eq_le ux. have xu : x <= u. by apply: ltW; rewrite ltNge ux. have := (sl _ _ cx xu ud'). rewrite qu0 xr subrr -(mulr0 k) ler_pmul2l // subr_le0 => ux'. by apply/eqP; rewrite eq_le ux'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc