proposition: Lemma min_roots_on p a b x s : all (> x) s -> roots_on p `]a, b[ (x :: s) -> [/\ x \in `]a, b[, roots_on p `]a, x[ [::], root p x & roots_on p `]x, b[ s].
proof: Proof. move=> lxs hxs. have hx: x \in `]a, b[ by rewrite (roots_on_in hxs) ?mem_head. rewrite hx (roots_on_root hxs) ?mem_head //. split=> // y; move: (hxs y); rewrite ?in_nil ?in_cons /=. case hy: (y \in `]a, x[)=> //=. rewrite (subitvPr _ hy) /<=%O /= ?lt_eqF ?(itvP hx) ?(itvP hy) //= => ->. by apply/negP; move/allP: lxs=> lxs /lxs; rewrite ?(itvP hy). case: eqVneq => [-> _|eyx]. by rewrite boundl_in_itv; apply/esym/negP; move/(allP lxs); rewrite ltxx. case: root; rewrite !(andbT, andbF) // !in_itv /=. case: (boolP (y \in s)) (allP lxs y) => [_ /(_ isT) -> /andP [] // | ys _]. by apply/contraFF => /andP [xy ->]; rewrite (lt_trans _ xy) ?(itvP hx). 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)