proposition: Lemma derp_root : a <= b -> 0 \in `]p.[a], p.[b][ -> { r : R | [/\ forall x, x \in `[a, r[ -> p.[x] < 0, p.[r] = 0, r \in `]a, b[ & forall x, x \in `]r, b] -> p.[x] > 0] }.
proof: Proof. move=> leab hpab. have /eqP hs : sgr p.[a] * sgr p.[b] == -1. by rewrite -sgrM sgr_cp0 pmulr_llt0 ?(itvP hpab). case: (ivt_sign leab hs) => r arb pr0; exists r; split => //; last 2 first. - by move/eqP: pr0. - move=> x rxb; have hd : forall t, t \in `]r, b[ -> 0 < (p^`()).[t]. by move=> t ht; rewrite der_pos // ?(subitvPl _ ht) /<=%O //= ?(itvP arb). by rewrite (le_lt_trans _ (derpr hd _)) ?(eqP pr0). - move=> x rxb; have hd : forall t, t \in `]a, r[ -> 0 < (p^`()).[t]. by move=> t ht; rewrite der_pos // ?(subitvPr _ ht) /<=%O //= ?(itvP arb). by rewrite (lt_le_trans (derpl hd _)) ?(eqP pr0). 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)