proposition: Lemma in_roots p (a b x : R) : (x \in roots p a b) = [&& root p x, x \in `]a, b[ & p != 0].
proof: Proof. case: rootsP=> //=; first by rewrite in_nil !andbF. by move=> p0 hr sr; rewrite andbT -hr andbC. 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)