proposition: Lemma cat_roots_on (p : {poly R}) a b x : x \in `]a, b[ -> ~~ (root p x) -> forall s s', sorted <%R s -> sorted <%R s' -> roots_on p `]a, x[ s -> roots_on p `]x, b[ s' -> roots_on p `]a, b[ (s ++ s').
proof: Proof. move=> hx /= npx0 s; elim: s a hx => [|y s ihs] a hx s' //= ss ss'. move/roots_on_nil=> hax hs' y; rewrite -hs' (itv_splitUeq hx). case: eqP => [->|_]; rewrite ?(negPf npx0) ?andbF //=. by case: (boolP (y \in `]a, x[)) => [/hax/negPf ->|]; rewrite ?andbF. move/min_roots_on; rewrite (order_path_min lt_trans) //. case=> // hy hay py0 hs hs' z. rewrite in_cons (@itv_splitUeq _ _ y); last first. by rewrite (subitvPr _ hy) /<=%O //= (itvP hx). have [->|ezy] := eqVneq; rewrite ?orbT //= -(ihs y) //. - by case: (z \in `]y, b[); rewrite ?orbF ?orbT //= (hay z). - by rewrite in_itv /= (itvP hx) (itvP hy). - exact: path_sorted ss. 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)