proposition: Lemma one_root_reciprocal (p: {poly R}) deg : (0 < size p)%N -> (size p <= deg.+1)%N -> one_root2 (recip deg p) 1 -> one_root1 p 0 1.
proof: Proof. move=> s0 sz [x1k [/andP []]]. set x1 := x1k.1; set k := x1k.2; set q := (recip deg p). move => x1gt1 kp neg sl. have x10 : 0 < x1 by apply: lt_trans x1gt1; exact: ltr01. set y' := x1 - q.[x1] / k. have nx1 : q.[x1] < 0 by rewrite neg //x1gt1 lexx. have knz: k != 0 by move: kp; rewrite lt0r; case /andP =>[]. have y'1: x1 < y' by rewrite /y' ltr_addl oppr_gt0 pmulr_llt0 // ?invr_gt0. have y'pos : 0 <= q.[y']. have aux: x1 <= x1 <= y' by rewrite (lexx x1) (ltW y'1). rewrite - (ler_add2r (- q.[x1])) add0r; apply: le_trans (sl _ _ aux). by rewrite /y' (addrC x1) addrK mulrN mulrC mulfVK. move: (@diff_xn_ub R deg 1); set u := _ *+ _; move => up. set u':= Num.max 1 u. have uu': u <= u' by rewrite le_maxr lexx orbT. have u1: 1 <= u' by rewrite le_maxr lexx. have u'0 : 0 < u' by rewrite (lt_le_trans ltr01). have divu_ltr : forall x, 0 <= x -> x / u' <= x. move => x x0; rewrite ler_pdivr_mulr // ler_pemulr //. have y'0: 0 < y' by apply: lt_trans y'1. pose y := y' + 1. have y'y : y' < y by rewrite /y ltr_addl. have y1 : x1 < y by apply: lt_trans y'1 _. have ypos : 0 < q.[y]. have aux: x1 <= y' <= y by rewrite (ltW y'1) (ltW y'y). rewrite (le_lt_trans y'pos) // -subr_gte0. by apply: lt_le_trans (sl _ _ aux); rewrite mulr_gt0 // subr_gt0. have y0: 0 < y by apply: lt_trans y'y. pose k' := half ((k * x1 ^+ 2 * y ^- 1 ^+ deg)). have k'p : 0 < k'. apply: half_gt0; rewrite mulr_gt0 //; first by rewrite mulr_gt0 // exprn_gt0. rewrite exprn_gt0 // invr_gt0 //. pose e := k' / u'. have ep: 0 < e by rewrite /e; apply: mulr_gt0 => //; rewrite invr_gt0. pose e1 := half e. have e1p : e1 > 0 by apply: half_gt0. have e1e : e1 < e by apply: half_ltx. move: (constructive_ivt y'1 nx1 y'pos e1p)=> [pv]. rewrite (surjective_pairing pv); set a:=pv.1;set b' := pv.2. move=> /and5P[/and3P [cla _ clb'] /and3P[x1a ab b'y'] nega posb' _]. move: (pol_lip q (z:=y)); set c := (norm_pol q^`()).[y] => cp. have cp0 : 0 < c. move: (lt_le_trans nega posb'); rewrite - subr_gt0 => dp. move: (ltW (le_lt_trans b'y' y'y)) => pb. move: y0; rewrite -oppr_lt0 => yn0. move: (ltW (lt_trans yn0 (lt_le_trans x10 x1a))) => pa. move: (cp _ _ pa (ltW ab) pb); rewrite (gtr0_norm dp) => dp'. by move: (lt_le_trans dp dp'); rewrite pmulr_lgt0 // subr_gt0. set b := Num.min y (b' +(half e1)/c). have blty: b <= y by rewrite /b le_minl lexx. have b'b: b' < b. rewrite lt_minr (le_lt_trans b'y' y'y) /= - ltr_subl_addl addrN. by rewrite (divr_gt0 (half_gt0 e1p) cp0). have clb:c * (b - b') < e1. apply: le_lt_trans (half_ltx e1p). by rewrite - (ler_pdivl_mull _ _ cp0) mulrC ler_subl_addl le_minl lexx orbT. pose n := (size p).-1. have a0 : 0 < a by apply: lt_le_trans x1a. have b'0 : 0 < b' by apply: lt_trans ab. have b0 : 0 < b by apply: lt_trans b'b. have ibp: 0 < b^-1 by rewrite invr_gt0. have inv_mono: forall x, 0 < x -> Num.sg (q.[x]) = Num.sg (p.[x^-1]). move => x xp. rewrite /q /recip. rewrite hornerM (horner_reciprocal _ ( unitf_gt0 xp)) hornerXn. rewrite !sgrM gtr0_sg ?mul1r //. by rewrite gtr0_sg // ?mul1r // exprn_gt0. by rewrite exprn_gt0. rewrite /one_root1 /pos_in_interval /neg_in_interval1. have res1:pos_in_interval 0 b^-1 (horner p). move => x /andP[x0 xb]. rewrite -[x]invrK -sgr_cp0 - inv_mono ?invr_gt0 // sgr_cp0. rewrite (le_lt_trans posb') // -subr_gte0 /=. have b'x : b' < x^-1. by rewrite inv_comp// (le_lt_trans xb)// ltf_pinv. have aa:x1 <= b' <= x^-1 by rewrite (ltW (le_lt_trans x1a ab)) (ltW b'x). by apply:lt_le_trans (sl _ _ aa); rewrite mulr_gt0 // subr_gt0. have res2: neg_in_interval1 a^-1 1 (horner p). move => x /andP[a1x xlt1]. have x0 : 0 < x by apply: lt_trans a1x; rewrite invr_gt0. have xv0 : 0 < x^-1 by rewrite invr_gt0. rewrite -[x]invrK -sgr_cp0 - inv_mono ?invr_gt0 // sgr_cp0. have x1a0 : x^-1 < a by rewrite inv_compr. case : (lerP x1 x^-1) => cmp; last first. apply: neg => //;rewrite (inv_comp ltr01 x0) invr1. by rewrite xlt1 (ltW cmp). have aux: (x1 <= x^-1 <= a) by rewrite cmp (ltW x1a0). apply: lt_trans nega; rewrite -subr_gte0. apply: lt_le_trans (sl _ _ aux). by rewrite mulr_gt0 // subr_gt0. exists b^-1, a^-1, k'. split => //. rewrite k'p ibp ltf_pinv// (inv_compr ltr01 a0) invr1. by rewrite (lt_trans ab b'b) (lt_le_trans x1gt1 x1a). move => x z bvx xz zav. rewrite le_eqVlt in xz; move/orP: xz => [xz | xz]. by rewrite (eqP xz) !addrN mulr0 lexx. have x0: 0 < x by apply: (lt_le_trans ibp bvx). have z0 : 0 < z by apply: (lt_trans x0). have lmrec : forall yy, 0 < yy -> p.[yy] = yy ^+ deg * q.[yy^-1]. move => yy yy0. rewrite hornerM horner_reciprocal1 ?unitf_gt0 // hornerXn exprVn mulrA. case h : (size p == 1)%N. rewrite (eqP h) !subSS !subn0 mulfV // expf_neq0 //. by move: yy0; rewrite lt0r; case/andP. have h' : size p = (size p).-2.+2. case h'': (size p) => [ | [ | sp]] //. by move: s0; rewrite h'' ltn0. by move: h; rewrite h'' eqxx. rewrite -expfB; last first. rewrite h' subSS prednK; last by rewrite h'. rewrite -{2}[deg]subn0 ltn_sub2l //. by rewrite -ltnS (leq_trans _ sz) // h'. by rewrite h'. by rewrite h' !subSS subKn ?subn0 // -ltnS -h'. rewrite (lmrec x x0) (lmrec z z0). set s := deg. set t1 := (x ^+ s - z ^+ s) * q.[x^-1]. set t3 := q.[x^-1] - q.[z^-1]. rewrite (_ : _ * _ - _ = t1 + t3 * z ^+ s); last first. by rewrite /t1 !mulrDl !mulNr ![_.[_] *_]mulrC !addrA addrNK. set t2 := t3 * _. pose k1 := -k'; pose k2 := k' + k'. have k2p : k2 = (k * x1 ^+ 2 * y ^-1 ^+ s) by apply: double_half. rewrite (_ : k' = k1 + k2); last by rewrite /k1 /k2 addrA addNr add0r. have xzi: z^-1 < x^-1 by rewrite ltf_pinv. have pa : x1 <= z^-1. by rewrite (le_trans x1a)// -(invrK a)// lef_pinv// posrE invr_gt0. have pb: x1 <= x^-1 by rewrite (ltW (le_lt_trans pa xzi)). have pc: 0 <= k * (x^-1 - z^-1) by apply: ltW;rewrite(mulr_gt0 kp) // subr_gt0. have pdd:(x1 <= z^-1 <= x^-1) by rewrite pa (ltW xzi). have pd:= (sl _ _ pdd). have t3p:= le_trans pc pd. have pe : 0 <= y^-1 <= z. by rewrite invr_ge0 ltW //= (le_trans _ (ltW xz))// (le_trans _ bvx)// lef_pinv. case /andP: (pow_monotone s pe) => _ hh. have maj' : t3 * y^-1 ^+ s <= t3 * z^+ s by rewrite ler_wpmul2l. rewrite mulrDl; apply: ler_add; last first. apply: le_trans maj'; rewrite /t3 k2p mulrAC. rewrite ler_pmul2r; last by apply: exprn_gt0; rewrite invr_gt0. apply: le_trans pd. rewrite ![k * _]mulrC mulrAC ler_pmul2r //. have xn0 : (x != 0) by move: x0; rewrite lt0r; case /andP =>[]. have zn0 : (z != 0) by move: z0; rewrite lt0r; case /andP =>[]. have xVn0 : (x^-1 != 0) by move: x0; rewrite -invr_gt0 lt0r; case /andP =>[]. rewrite -[x^-1](mulfK zn0) -(mulrC z) - (mulrA z _ _). rewrite -{2}[z^-1](mulfK xn0) -(mulrA _ x _)(mulrCA _ x). rewrite (mulrC z^-1) -mulrBl (mulrC (z - x)). rewrite ler_pmul2r /=; last by rewrite subr_gte0. apply: le_trans (_ : x1 / z <= _); first rewrite ler_pmul2l //=. by rewrite ler_pmul2r ?invr_gt0. move:(ltW xz) => xz'. have xzexp : (x ^+ s - z ^+ s) <= 0. have aux: 0 <=x <= z by rewrite xz' ltW//. by case /andP :(pow_monotone s aux)=> [_]; rewrite subr_le0. have xzexp' : (z ^+ s - x ^+ s) >= 0 by rewrite subr_ge0 - subr_le0. rewrite /t1 /k1 /k' {maj' t2 t3}. case: (lerP 0 ( q.[x^-1])) => sign; last first. apply: le_trans (_ : 0 <= _). by rewrite mulNr lter_oppl oppr0 mulr_ge0 //?(ltW k'p)// subr_gte0 /= ltW. by rewrite mulr_le0 // ltW. rewrite mulNr lter_oppl -mulNr opprD opprK addrC. have rpxe : q.[x^-1] <= e. have bvx' : x^-1 <= b by rewrite -(invrK b)// lef_pinv. apply: (@le_trans _ _ q.[b]). have aux:(x1 <= x^-1 <= b) by rewrite pb bvx'. rewrite -subr_ge0 /= ;apply: le_trans (sl _ _ aux). rewrite mulr_ge0 ?subr_gte0 // ltW //. rewrite -[_ _ b]addr0 -(addrN (q).[b']) addrA. rewrite (addrC ( _ b)) -addrA - (double_half e) (ler_add clb')//. have yb: - y <= b' by apply: ltW; apply: lt_trans b'0; rewrite oppr_lt0. move: (le_trans (cp b' b yb (ltW b'b) blty) (ltW clb)). by move /ler_normlP => [_]. apply: le_trans (_ : (z^+ s - x ^+ s) * e <= _). by rewrite ler_wpmul2l // ?subr_gte0. have un0 : (u' != 0) by move: u'0; rewrite lt0r; case /andP =>[]. rewrite [_ * e]mulrC; apply: le_trans (_ : e * (u' * (z - x)) <= _)=> /=. apply: ler_wpmul2l; first exact: ltW. apply: (@le_trans _ _ (u * (z - x))). have xm1: -1 <= x by exact: (ltW (lt_trans (ltrN10 R) x0)). have a1 : 1 <= a by apply: (ltW (lt_le_trans x1gt1 x1a)). rewrite - (ger0_norm xzexp'); apply: (up _ _ xm1 xz'). apply: le_trans zav _. by rewrite invr_le1 // unitf_gt0. by rewrite ler_pmul2r // subr_gte0. rewrite mulrA ler_pmul2r; last by rewrite subr_gte0. rewrite /= /e divfK ?lterr //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol