proposition: Lemma roots_cons p a b x s : (roots p a b == x :: s) = [&& p != 0, x \in `]a, b[, roots p a x == [::], root p x & roots p x b == s].
proof: Proof. case: rootsP => //= p0 hs' ps'. apply/idP/idP. move/eqP=> es'; move: ps' hs'; rewrite es' /= => sxs. case/min_roots_on; first by apply: order_path_min=> //; apply: lt_trans. move=> -> rax px0 rxb. rewrite px0 (@roots_uniq p a x [::]) // (@roots_uniq p x b s) ?eqxx //=. by move/path_sorted:sxs. case: rootsP p0=> // p0 rax sax _. case/and3P=> hx hax; rewrite (eqP hax) in rax sax. case: rootsP p0=> // p0 rxb sxb _. case/andP=> px0 hxb; rewrite (eqP hxb) in rxb sxb. rewrite [_ :: _](@roots_uniq p a b) //; last first. rewrite /= path_min_sorted //; apply/allP => y. by rewrite -(eqP hxb); move/roots_in/itvP->. move=> y; rewrite (itv_splitUeq hx) !andb_orl in_cons. have [->|_] := eqVneq y x; first by rewrite px0 orbT. by rewrite andFb orFb rax rxb in_nil. 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)