proposition: Lemma no_root_roots (p : {poly R}) a b : {in `]a, b[ , noroot p} -> roots p a b = [::].
proof: Proof. move=> hr; case: rootsP => // p0 hs ps. apply: (@roots_on_uniq p a b)=> // x; rewrite in_nil. by apply/negP; case/andP => /hr/negPf->. 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)