proposition: Lemma roots_nil p a b : p != 0 -> roots p a b = [::] -> {in `]a, b[, noroot p}.
proof: Proof. case: rootsP => // p0 hs ps _ s0 x axb. by move: (hs x); rewrite s0 in_nil !axb /= => ->. 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)