proposition: Lemma path_roots p a b : path <%R a (roots p a b).
proof: Proof. case: rootsP=> //= p0 hp sp; rewrite path_min_sorted //. by apply/allP=> y; rewrite -hp; case/andP => /itvP ->. 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)