proposition: Lemma roots_uniq p a b s : p != 0 -> roots_on p `]a, b[ s -> sorted <%R s -> s = roots p a b.
proof: Proof. case: rootsP=> // p0 hs' ps' _ hs ss. exact: (@roots_on_uniq p a b)=> //. 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)