proposition: Lemma monotonic_rootN (p : {poly R}) (a b : R) : {in `]a, b[, noroot p^`()} -> ((roots_on p `]a, b[ [::]) + ({r : R | roots_on p `]a, b[ [:: r]}))%type.
proof: Proof. move=> hp'; case: (ltrP a b); last first => leab. by left => x; rewrite in_nil itv_ge // -leNgt. wlog {hp'} hp'sg: p / forall x, x \in `]a, b[ -> sgr (p^`()).[x] = 1. move=> hwlog; move: (mid_in_itvoo leab) (polyrN0_itv hp') => hm /(_ _ _ hm). case: (sgrP _.[mid a b])=> hpm. - by move: (hp' _ hm); rewrite rootE hpm eqxx. - by move/(hwlog p). - move=> hp'N; case: (hwlog (-p))=> [x|h|[r hr]]. * by rewrite derivE hornerN sgrN=> /hp'N->; rewrite opprK. * by left; apply: roots_on_opp. * by right; exists r; apply: roots_on_opp. have hp'pos x : x \in `]a, b[ -> (p^`()).[x] > 0. by move=> /hp'sg /eqP; rewrite sgr_cp0. case: (lerP 0 p.[a]) => ha. left; apply: no_roots_on => x axb; rewrite rootE gt_eqF //. by rewrite (le_lt_trans _ (derpr hp'pos _))// (subitvPr _ axb) /<=%O /=. case: (lerP p.[b] 0) => hb. left => x; case: (boolP (x \in _)) => //= axb; rewrite rootE lt_eqF //. by rewrite (lt_le_trans (derpl hp'pos _)) // (subitvPl _ axb) /<=%O /=. case: (derp_root hp'pos (ltW leab) _) => [|r [h1 h2 h3] h4]; first exact/andP. right; exists r => x; rewrite in_cons in_nil (itv_splitUeq h3). have [->|exr] := eqVneq; rewrite ?orbT ?orbF /=; first by apply/eqP. case: rootP => px0; rewrite (andbT, andbF) //; apply/negP; case/orP=> hx. by move: (h1 x); rewrite (subitvPl _ hx) /<=%O //= px0 ltxx; move/implyP. by move: (h4 x); rewrite (subitvPr _ hx) /<=%O //= px0 ltxx; move/implyP. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)