proposition: Lemma desc_l4 (p: {poly R}) : alternate_1 p -> inv2 p.
proof: Proof. move: p;elim/poly_ind => [| p a ih]; first by rewrite/alternate_1 polyseq0. have desc_c: alternate_1 (a%:P) -> inv2 (a%:P). rewrite polyseqC;case (a==0) => //=; case ha: (0< a) => // _. move=> eps eps0; exists (eps / a); split. by move => y _ _; rewrite !hornerC. by move => y1 y2 _ _ _ ; rewrite !hornerC. by rewrite hornerC ha divr_gt0 //= (divrK (unitf_gt0 ha)). case sp : (nilp p). by move: sp; rewrite nil_poly; move /eqP => ->; rewrite mul0r add0r. rewrite -{1} cons_poly_def polyseq_cons sp /=. case: (ltrgtP 0 a) => ha. move => haposp eps eps0; rewrite /inv2 /=. have : all_ge0 (p * 'X + a%:P). by rewrite -cons_poly_def polyseq_cons sp /= ltW. move/all_pos_inv/(_ eps eps0)=> [x [h1x h2x /andP[h3x h4x]]]; exists x. have xp:= ltW h3x. split => //; rewrite h3x h4x !hornerE ltr_spaddr // mulr_ge0 //. by rewrite all_pos_positive. rewrite -oppr_gt0 in ha. set q := (p * 'X + a%:P). move=> il;move: (ih il _ ((half_gt0 ha)))=> [x [H1 H2 /and3P [xp xpx xe]]]. move: (le_lt_trans xe (half_ltx ha)) => xe'. have qxn : q.[x] < 0 by rewrite !hornerE mulrC -(opprK a) subr_lt0. move: (maxS x (-a/p.[x])) => /andP []; set y := (_ + _) => yx val. have yx':= ltW yx. have ppos: forall t, x <= t -> 0 < p.[t]. move => t xt;exact (lt_le_trans xpx (H2 _ _ (lexx x) xt xt)). have qsincr: forall t d, x <= t -> 0 < d -> q.[t] < q.[t+d]. move => t d xt dp; rewrite !hornerE. set w := _ + _. have aux: t <= t+d by rewrite - {1}(addr0 t) ler_add2l ltW. have xtd:= (le_trans xt aux). rewrite mulrDr -addrAC addrC ltr_spaddl ?(mulr_gt0 (ppos _ xtd) dp)//. rewrite !ler_add2r (ler_pmul2r (lt_le_trans xp xt)). by apply:H2 => //. have qincr: forall t, x<=t -> {in <=%R t &, pol_increasing q}. move => t xt u v ut vt; rewrite le_eqVlt; case /orP => uv. by move /eqP:uv => ->. rewrite ltW // - (addNKr u v); apply: (qsincr _ _(le_trans xt ut)). by rewrite addrC subr_gt0. move: (H2 _ _ (lexx x) yx' yx') => lepxpy. have yge0: 0 <= y by rewrite ltW // (lt_le_trans xp yx'). have posval : 0 <= q.[y]. rewrite !hornerE -(addNr a) /= ler_add2r /=. apply: (@le_trans _ _ (p.[x] * y)); last by rewrite ler_wpmul2r. rewrite // mulrC - ler_pdivr_mulr // ltW //. set r := ('X * q). have negval' : r.[x] < 0 by rewrite 2!hornerE pmulr_rlt0. have posval' : 0 <= r.[y] by rewrite 2! hornerE mulr_ge0. move=> epsilon Hepsilon /=. move: (half_gt0 Hepsilon) => he1. move: (constructive_ivt yx negval' posval' he1) => [ppr]. rewrite (surjective_pairing ppr); set u:=ppr.1;set v := ppr.2. move /and5P => [/and3P [_ _ smallv] /and3P[xd dv v'y] _ posv _]. have {xd dv} xv : x < v by apply: le_lt_trans xd dv. have pv : 0 < v by apply: lt_trans xv. move: posv; rewrite 2! hornerE -{1} (mulr0 v) (ler_pmul2l pv) => posv. move: (pol_cont r v he1) => [d' dp' pd']. pose d := half d'. have dp : d > 0 by rewrite half_gt0. have dd' : d < d' by apply: half_ltx. have vvd : v < v + d by rewrite ltr_addl /=. have xvd : x < v + d by apply: lt_trans vvd. have lvd : 0 < p.[v + d] by apply: ppos; exact: ltW. move => {y yx val yx' posval posval' v'y lepxpy yge0}. have pa: le_below_x (v + d) (horner q). move => y y0 yvd; rewrite !hornerE ler_add2r /=. case cmp: (y <= x); last first. have cmp': x <= y by rewrite ltW // ltNge cmp. apply: le_trans (_ : p.[v + d] * y <= _). by apply: ler_wpmul2r => //; apply: H2 => //;apply: (le_trans cmp'). by rewrite ler_wpmul2l // ltW. apply: le_trans (_ : p.[x] * y <= _). by rewrite ler_wpmul2r //; apply: H1. apply: le_trans (_ : p.[x] * (v + d) <= _); last first. rewrite ler_wpmul2r //; first exact: le_trans yvd. rewrite H2 //; first (by apply: (lexx x)); by apply:ltW. by rewrite ler_wpmul2l // ltW. exists (v + d). rewrite (le_lt_trans posv (qsincr _ _ (ltW xv) dp)) (lt_trans pv vvd). split => //=; first by apply: qincr; apply: ltW. rewrite - (double_half epsilon). apply: le_trans (_ : ((half epsilon) + r.[v+d] -r.[v]) <= _). rewrite [ half epsilon + _] addrC -addrA. rewrite [r.[v + d]] hornerE hornerX ler_addl subr_ge0 //. rewrite -! addrA ler_add2l. have aux:`|(v+d) - v| < d' by rewrite (addrC v) addrK ger0_norm// ltW. by move: (ltW (pd' _ aux)) => /ler_normlP [_]. move => halt1 eps eps0. move: (ih halt1 _ ltr01) => [x [plx pmonx /and3P [gx0 gpx0 lpx1]]]. have e1px : 0 < eps / x by apply: mulr_gt0=> //=; rewrite invr_gt0. move: (ih halt1 _ e1px) => [v [plv pmonv /and3P [gv0 gpv0 lpve]]]. rewrite -ha addr0. have aux: forall w, 0 <=w -> 0 <= p.[w] -> {in <=%R w &, pol_increasing p} -> {in <=%R w &, pol_increasing ((p * 'X))}. move => w wz pwz H s t sw tw st; rewrite !hornerE. move: (H _ _ sw tw st) (le_trans pwz (H _ _ (lexx w) sw sw)) => pa pb. by apply:(ler_pmul pb (le_trans wz sw) pa st). set w:= (Num.min x v); exists w. have wc: w = x \/ w = v. by rewrite /w /minr; case: ifPn; [left|right]. have wz: 0 < w by case wc => ->. have pw0: 0 < p.[w] by case wc => ->. rewrite wz 3! hornerE (pmulr_lgt0 _ wz) pw0. split. move => t tp tw; rewrite !hornerE mulrC (mulrC _ w). apply: (pmul2w1 tp (ltW pw0) tw). move: tp tw;case wc=> ->; [apply: plx | apply: plv]. by apply: aux; [apply: ltW | by apply: ltW| case wc => ->]. move: lpve; rewrite (ler_pdivl_mulr _ _ gx0) => lpve. case /orP:(le_total x v)=> xv; rewrite /w/=. move/min_idPr : (xv); rewrite minC => ->. apply: le_trans lpve; rewrite mulrA. rewrite (ler_pmul2r gx0);apply: (ler_pmul (ltW gx0) (ltW gpx0) xv). exact:(pmonx _ _ (lexx x) xv xv). move/min_idPr : (xv) => ->. apply: le_trans lpve. rewrite mulrA. by rewrite (ler_pmul2l (mulr_gt0 gv0 gpv0) v x). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol