proposition: Lemma rootsRP p a b : {in `]-oo, a], noroot p} -> {in `[b , +oo[, noroot p} -> roots p a b = rootsR p.
proof: Proof. move=> rpa rpb. have [->|p_neq0] := eqVneq p 0; first by rewrite rootsR0 roots0. apply: (irr_sorted_eq lt_trans); rewrite ?sorted_roots // => x. rewrite -roots_on_rootsR -?roots_on_roots //=. case: (boolP (root _ _)); rewrite ?(andbT, andbF) //. apply: contraLR; rewrite in_itv negb_and -!leNgt. by move=> /orP[/rpa //|xb]; rewrite rpb // in_itv andbT. 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)