proposition: Lemma desc (p: {poly R}): alternate p -> one_root2 p 0.
proof: Proof. move: p; elim/poly_ind => [| p a IHl]; first by rewrite polyseq0. rewrite -cons_poly_def polyseq_cons. case sl: (nilp p) => /=. by rewrite polyseqC; case: (a == 0) => //=;rewrite ! if_same. case: (ltrP a 0) => ha alt1. rewrite - oppr_gt0 in ha. move: (desc_l4 alt1 (half_gt0 ha)) => [x [psub pmon /and3P [xp pxp pxa1]]]. move: (le_lt_trans pxa1 (half_ltx ha)) => pxa2. exists (x, p.[x]); simpl; rewrite xp pxp; split => //. move => y /andP [posy yx]. move: (ltW posy) => posy'. rewrite horner_cons -(opprK a) subr_lt0; apply: le_lt_trans pxa2. rewrite mulrC; apply:(pmul2w1 posy' (ltW pxp) yx (psub _ posy' yx)). move => y z xyz;rewrite !horner_cons opprD addrCA addrK. rewrite [_ + _ * _]addrC [_ * z]mulrC [_ * y]mulrC. have slp:slope_bounded x 0 (horner p). move => t u /andP[xt tu];rewrite mul0r subr_gte0 pmon //. exact (le_trans xt tu). move:(slope_product_x (ltW xp) (lexx 0) slp xyz). move/andP :xyz => [xy yz]. rewrite mulr0 add0r; apply: le_trans. by apply: (ler_wpmul2r _ (pmon _ _ (lexx x) xy xy)); rewrite subr_ge0. move: alt1; case a0 : (a == 0) => // alt1; move: (eqP a0) => a00. clear ha a0. move: (IHl alt1) => [v1k []] {IHl}. set v1 := v1k.1; set k:= v1k.2; simpl => /andP[v1pos kpos] low incr. have negval : (p.[v1] < 0) by apply: low; rewrite ?lexx v1pos. set k':= half (k * v1). have posk' : 0 < k' by apply: half_gt0; apply: mulr_gt0. set u := (- p.[v1]) / k. move: (maxS 0 u); set v:= Num.max 0 _ => /andP [pa pb]. set v2:= v1 + v +1. have v0: 0 <= v by rewrite le_maxr lexx. have v1v2: v1 < v2 by rewrite /v2 - addrA (ltr_addl v1). have pos1:0 <= p.[v1 + v]. move: (kpos); rewrite lt0r => /andP [ kne0 _]. move: kpos; rewrite - invr_gt0 => kpos. rewrite /v; have [caf|caf] := leP u 0. by rewrite addr0 - oppr_le0 - (pmulr_lle0 _ kpos). case/orP:(le_total u 0); [ | move => up]. by rewrite leNgt caf. have aa: v1 <= v1 <= v1 + u by rewrite lexx ler_addl. rewrite - (ler_addr (- p.[v1]));apply: le_trans (incr _ _ aa). by rewrite (addrC v1) addrK /u (mulrC _ (k^-1)) mulVKf //. have pos : 0 < p.[v2]. have hh: v1 <= v1 + v <= v1 + v + 1 by rewrite !ler_addl v0 ler01. apply: (le_lt_trans pos1);rewrite -subr_gt0. by apply: (lt_le_trans _ (incr _ _ hh)); rewrite addrAC addrN add0r mulr1. clear v0 pos1 pa pb. move: (constructive_ivt v1v2 negval (ltW pos) posk') => [x12]. rewrite (surjective_pairing x12); set x1:=x12.1;set x2 := x12.2. move /and5P => [/and3P [x1close _ _] /and3P[v1x1 _ _] px1neg _ _]. have x1pos : 0 < x1 by apply: lt_le_trans v1x1. have Plow : forall x, 0 < x -> x <= x1 -> x * p.[x] < 0. move=> x xpos xx1; rewrite (pmulr_rlt0 _ xpos). case: (ltrP x v1)=> xv1; first by apply: low=> //; rewrite xpos ltW. apply: le_lt_trans px1neg. move: xx1; rewrite le_eqVlt; move/orP => [xx1 | xlx1]; first by rewrite (eqP xx1) lexx. have aux : v1 <= x <= x1 by rewrite xv1 ltW. rewrite -subr_gte0; move: (incr _ _ aux); apply: le_trans. by apply: ltW; apply: mulr_gt0 => //; rewrite subr_gt0. exists (x1,k'); simpl; rewrite x1pos posk'; split => //. by move=> x /andP[x0 xx1]; rewrite horner_cons a00 addr0 mulrC;apply : Plow. move => x y /andP[x1x xy]. rewrite ! horner_cons a00 !addr0 (mulrC _ x) (mulrC _ y). have: (v1 * k + p.[x]) * (y - x) <= y * p.[y] - x * p.[x]. apply:(slope_product_x (ltW v1pos) (ltW kpos) incr). by rewrite xy (le_trans v1x1 x1x). apply: le_trans; rewrite ler_wpmul2r //; first by rewrite subr_ge0. rewrite mulrC - (double_half (k * v1 )) -/k' - addrA ler_addl. rewrite - (opprK k') addrC subr_gte0 (le_trans x1close) // -subr_gte0. have: k * (x - x1) <= p.[x] - p.[x1] by apply: incr =>//; rewrite x1x v1x1. by apply : le_trans; apply: mulr_ge0 => //; rewrite ?(ltW kpos) ?subr_ge0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol