proposition: Lemma max_roots_on p a b x s : all (< x) s -> roots_on p `]a, b[ (x :: s) -> [/\ x \in `]a, b[, roots_on p `]x, b[ [::], root p x & roots_on p `]a, x[ s].
proof: Proof. move/allP=> lsx /roots_on_comp/=/min_roots_on[]. apply/allP=> y; rewrite -[y]opprK (mem_map oppr_inj). by move/lsx; rewrite ltr_opp2. rewrite oppr_itv root_comp !hornerE !opprK=> -> rxb -> rax. by split=> //; apply/roots_on_comp. 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)