proposition: Lemma one_root_reciprocate {R : archiFieldType} (l : {poly R}) : one_root2 (reciprocal_pol l) 1 -> one_root1 l 0 1.
proof: Proof. move=> [x1 [k [x1gt1 kp neg sl]]]. have x10 : (0 < x1)%R by rewrite (lt_trans _ x1gt1)// ltr01. set y' := x1 - (reciprocal_pol l).[x1] / k. have y'1 : x1 < y'. rewrite /y' -(ltr_add2l (-x1)) addNr addrA addNr add0r -mulNr. by rewrite divr_gt0 // oppr_gt0; exact: neg. have nx1 : (reciprocal_pol l).[x1] < 0%R by apply: neg; rewrite // ltxx. have y'pos : (0 <= (reciprocal_pol l).[y'])%R. rewrite -[_ _ y']addr0 -{2}(addNr (reciprocal_pol l).[x1]) addrA -{2}(opprK (_ _ x1)) subr_gte0 /=. apply: le_trans (_ : k * (y' - x1) <= _)=> /=. by rewrite /y' (addrC x1) addrK mulrN mulrC mulrVK // unitfE gt_eqF. exact: sl. have [u u0 up] := diff_xn_ub (size l - 1) _ (@ltr01 R). have [u' u1 u'u] : exists2 u', (1 <= u')%R & (u <= u')%R. case cmp: (1 <= u)%R; first by exists u => //; rewrite lexx cmp. by exists 1%R; rewrite ?lexx // ltW // ltNge cmp. have u'0 : (0 < u')%R by apply: lt_le_trans u1. have divu_ltr (x : R) : (0 <= x)%R -> (x / u' <= x)%R. by move=> x0; rewrite ler_pdivr_mulr// ler_pemulr. have y'0 : (0 < y')%R by apply: lt_trans y'1. pose y := y' + 1. have y'y : y' < y by rewrite /y ltr_addl ltr01. have y1 : x1 < y by apply: lt_trans y'1 _. have ypos : (0 < (reciprocal_pol l).[y])%R. apply: le_lt_trans y'pos _=> /=. rewrite -subr_gte0 /=; apply: lt_le_trans (_ : k * (y - y') <= _)=> /=. by rewrite mulr_gt0// subr_gt0. by apply: sl=> //; apply: ltW. have y0 : (0 < y)%R by apply: lt_trans y'y. pose k' := ((k * x1 ^+ 2 * y ^- 1 ^+ (size l - 1))/(1+1)). have k'p : (0 < k')%R. rewrite /k' !mulr_gt0// ?invr_gt0 ?addr_gt0 ?ltr01//. by rewrite exprn_gt0// invr_gt0. pose e : R := k' / u'. have ep: (0 < e)%R by rewrite divr_gt0. have [e1 [e2 [e1p e2p e1e2e e1e e2e]]] := cut_epsilon _ ep. have [[a b']] := @constructive_ivt _ (@reciprocal_pol _ l) _ _ _ y'1 nx1 y'pos e1p. rewrite {1}/pair_in_interval. move=> /and5P[/and3P[cla ? clb']]. rewrite /pair_in_interval. move=> /and3P[x1a ab b'y' nega posb' bma]. have [c cp] := cm3 y y0 (reciprocal_pol l). have a0 : (0 < a)%R by apply: lt_le_trans x1a. have c0 : (0 < c)%R. rewrite -(@pmulr_lgt0 _ (b' - a)) ?subr_gt0//. rewrite (@lt_le_trans _ _ (`|(reciprocal_pol l).[b'] - (reciprocal_pol l).[a] |))//; last first. apply: cp. - exact: ltW. - exact: ltW. - by rewrite (le_trans b'y')// ltW. by rewrite normr_gt0// gt_eqF// subr_gt0. have [b [b'b clb blty]] : exists b, [/\ b' < b, c * (b - b') < e2 & b <= y]. have [e3 [e4 [e3p e4p e3e4e2 e3e2 e4e2]]] := cut_epsilon _ e2p. case cmp : (b' + e2 / c <= y). exists (b' + e3 / c); split. - by rewrite ltr_addl// divr_gt0. - by rewrite (addrC b') addrK mulrA (mulrC c) mulfK // gt_eqF. - apply: le_trans cmp; rewrite ler_add2l//. by rewrite ler_pmul// ltW// invr_gt0. exists y; split => //. - by rewrite (le_lt_trans b'y'). - by rewrite mulrC -ltr_pdivl_mulr// ltr_subl_addl ltNge cmp. pose n := ((size l))%:R - 1. have b'0 : (0 < b')%R by apply: lt_trans ab. have b0 : (0 < b)%R by apply: lt_trans b'b. have b'v0 : (0 < b'^-1)%R by rewrite invr_gte0. have bv0 : (0 < b^-1)%R by rewrite invr_gte0. have bb'v : b^-1 < b'^-1 by rewrite ltf_pinv. exists b^-1, a^-1, k'; split => //. - split => //. + by rewrite (lt_le_trans bb'v)// lef_pinv// ltW. + by rewrite invf_lt1// (lt_le_trans _ x1a). - move => x x0 xb. have xv0 : (0 < x^-1)%R by rewrite invr_gt0. have xexp0 : (0 < x^-1 ^+ (size l - 1))%R by rewrite exprn_gt0. have b'x : b' < x^-1. by rewrite -(invrK b')// ltf_pinv// (le_lt_trans _ bb'v). rewrite -(pmulr_rgt0 _ xexp0) -{2}[x]invrK -horner_reciprocal; last first. by rewrite unitfE gt_eqF. apply: (le_lt_trans posb'); rewrite -subr_gte0 /=. apply: lt_le_trans (_ : k * (x^-1 - b') <= _)=> /=. by rewrite mulr_gt0// subr_gt0. by apply: sl => //; rewrite (le_trans x1a)// ltW. - move => x a1x xlt1. have x0 : (0 < x)%R by apply: lt_trans a1x; rewrite invr_gt0. have xv0 : (0 < x^-1)%R by rewrite invr_gt0. have x1a0 : (x^-1 < a)%R by rewrite -[a]invrK ltf_pinv// posrE// invr_gt0. have xexp0 : (0 < x^-1 ^+ (size l - 1))%R by apply: exprn_gt0. rewrite -(pmulr_rlt0 _ xexp0) -{2}[x]invrK -horner_reciprocal//; last first. by rewrite unitfE gt_eqF. case cmp: (x^-1 <= x1); last (move/negbT:cmp => cmp). by apply: neg => //; rewrite -invr1 ltf_pinv// ?posrE ltr01//. apply: lt_trans nega; rewrite -subr_gte0. apply: lt_le_trans (_ : k * (a - x^-1) <= _). by rewrite mulr_gt0// subr_gt0. apply: sl => //. rewrite -ltNge in cmp. exact: ltW. - move=> x z bvx + zav; rewrite le_eqVlt => /predU1P[->|xz]. by rewrite !addrN mulr0 lexx. have x0 : (0 < x)%R by apply: lt_trans bvx. have z0 : (0 < z)%R by apply: (lt_trans x0). have := horner_reciprocal1 l (unitf_gt0 x0) => ->. have := horner_reciprocal1 l (unitf_gt0 z0) => ->. rewrite (_ : _ * _ - _ = (x ^+ (size l - 1) - z ^+ (size l - 1)) * (reciprocal_pol l).[x ^-1] + ((reciprocal_pol l).[x ^-1] - (reciprocal_pol l).[z ^-1]) * z ^+ (size l - 1)); last first. by rewrite !mulrDl !mulNr ![_.[_] * _]mulrC !addrA addrNK. set t1 := _ * _.[_]. set t3 := (_.[_] - _). set t2 := t3 * _. pose k1 := -k'; pose k2 := k' + k'. have times2 : forall a : rat, a + a = (1 + 1) * a. by move => a'; rewrite mulrDl !mul1r. have k2p : k2 = (k * x1 ^+ 2 * y ^-1 ^+ (size l - 1)). rewrite /k2 /k' -mulr2n -mulr_natl. rewrite -(mulrC (1 + 1)^-1) mulrA mulfV; first by rewrite mul1r. have twop : (0 < (1 + 1))%Q by []. by rewrite gt_eqF// ltr0n. rewrite (_ : k' = k1 + k2); last by rewrite /k1 /k2 addrA addNr add0r. have x1ltvz : x1 < z ^-1. by rewrite (le_lt_trans x1a) // -[a]invrK ltef_pinv ?posrE ?invr_gt0 ?ltW. rewrite mulrDl; apply: ler_add; last first. have maj' : t3 * y^-1 ^+ (size l - 1) <= t3 * z^+ (size l - 1). have maj : y^-1 ^+(size l - 1) <= z ^+ (size l - 1). case: (size l - 1)%N => [ | n']; first by rewrite !expr0 lexx. have /pow_monotone : (0 <= y ^-1 <= z)%R. rewrite ltW /=; last by rewrite invr_gt0 (lt_trans x10). apply: ltW (le_lt_trans _ xz); apply: ltW (le_lt_trans _ bvx). by rewrite lef_pinv ?posrE. by move=> /(_ n'.+1) /andP[]. rewrite lter_pmul2l // /t3. apply: (lt_le_trans _ (_ : k * (x ^-1 - z ^-1) <= _)); last first. apply: sl; first by apply: ltW. by rewrite ltf_pinv. by rewrite mulr_gt0 // subr_gt0 ltf_pinv. apply: le_trans maj'; rewrite /t3 k2p mulrAC. rewrite lter_pmul2r; last by apply: exprn_gt0; rewrite invr_gt0. apply: ltW (lt_le_trans _ (_ :k * (x ^-1 - z ^-1) <= _)). rewrite ![k * _]mulrC mulrAC lter_pmul2r; last by []. rewrite -[x ^-1](mulrK (unitf_gt0 z0)). rewrite -[X in _ < _ - X](mulrK (unitf_gt0 x0)) -(mulrC x) -(mulrC z). rewrite (mulrAC x) -!(mulrA _ (x^-1)) -mulrBl (mulrC (z - x)). rewrite lter_pmul2r; last by rewrite subr_gte0. apply: lt_le_trans (_ : x1 / z <= _); first by rewrite lter_pmul2l. rewrite lter_pmul2r; last by rewrite invr_gte0. by apply: ltW (lt_trans x1ltvz _); rewrite ltef_pinv ?posrE. apply: sl; first by apply: ltW. by rewrite ltef_pinv ?posrE. rewrite /t1/k1/k' {t2 t3}. have xzexp : (x ^+ (size l - 1) <= z ^+ (size l - 1)). case sizep : (size l - 1)%N => [ | n']. by rewrite !expr0 ltexx. have /pow_monotone : (0 <= x <= z)%R. by rewrite !ltW. by move=>/(_ n'.+1)=> /andP[]. case: (lerP 0 ((reciprocal_pol l).[x^-1])) => sign; last first. apply: le_trans (_ : 0 <= _)%R. rewrite mulNr lter_oppl oppr0; apply: mulr_ge0; last first. by rewrite subr_gte0 ltW. exact (ltW k'p). by rewrite nmulr_lge0 // subr_lte0. rewrite mulNr lter_oppl -mulNr opprB. have rpxe : (reciprocal_pol l).[x^-1] <= e. apply:le_trans (_ : (reciprocal_pol l).[b] <= _) => /=. rewrite -subr_gte0 /= ; apply: le_trans (_ : k * (b - x^-1) <= _). rewrite mulr_ge0 //. exact: ltW. by rewrite subr_ge0 ltW // -(invrK b) ltef_pinv ?posrE. apply: sl. by apply: (ltW (lt_trans x1ltvz _)); rewrite ltef_pinv ?posrE. by rewrite -(invrK b) ltef_pinv ?posrE. rewrite -[_ _ b]addr0 -(addrN ((reciprocal_pol l).[b'])) addrA. rewrite (addrC (_.[b])) -addrA; apply: le_trans e1e2e. apply: ler_add; first by []. apply: (le_trans (ler_norm _)). by apply/ltW/(le_lt_trans _ clb)/cp=> //; apply/ltW. apply: le_trans (_ : (z^+ (size l - 1) - x ^+ (size l - 1)) * e <= _). move: xzexp; rewrite -subr_gte0 le_eqVlt => /predU1P[<-|xzexp] /=. by rewrite !mul0r. by rewrite lter_pmul2l. rewrite [_ * e]mulrC; apply: le_trans (_ : e * (u' * (z - x)) <= _)=> /=. rewrite ler_pmul2l//. apply: le_trans (_ : u * (z - x) <= _). apply: up => //. by apply: ltW. apply: ltW (lt_trans zav _). by rewrite invf_lt1 //; by apply: lt_le_trans x1a. by rewrite ler_pmul2r// subr_gt0. rewrite mulrA. rewrite ler_pmul2r// ?subr_gt0//. by rewrite /e divrK// unitfE gt_eqF. Qed.
imports: mathcomp(all_ssreflect all_algebra) pol desc