proposition: Lemma roots_on_rootsR p : p != 0 -> roots_on p `]-oo, +oo[ (rootsR p).
proof: Proof. rewrite /rootsR => p_neq0 x /=; rewrite -roots_on_roots // andbC. by have [/(cauchy_boundP p_neq0) /=|//] := rootP; rewrite ltr_norml. 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)