proposition: Lemma roots_rcons p a b x s : (roots p a b == rcons s x) = [&& p != 0, x \in `]a , b[, roots p x b == [::], root p x & roots p a x == s].
proof: Proof. case: rootsP; first by case: s. move=> // p0 hs' ps' /=. apply/idP/idP. move/eqP=> es'; move: ps' hs'; rewrite es' /= => sxs. have hsx: rcons s x =i x :: rev s. by move=> y; rewrite mem_rcons !in_cons mem_rev. move/(roots_on_same _ _ hsx). case/max_roots_on. move: sxs; rewrite -[rcons _ _]revK rev_sorted rev_rcons. by apply: order_path_min=> u v w /= /(lt_trans _); apply. move=> -> rax px0 /(@roots_on_same _ s); move/(_ (mem_rev _)) => rxb. rewrite px0 (@roots_uniq p x b [::]) // (@roots_uniq p a x s) ?eqxx //=. move: sxs; rewrite -[rcons _ _]revK rev_sorted rev_rcons. by move/path_sorted; rewrite -rev_sorted revK. 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 [rcons _ _](@roots_uniq p a b) //; last first. rewrite -[rcons _ _]revK rev_sorted rev_rcons /= path_min_sorted. by rewrite -rev_sorted revK. apply/allP=> y; rewrite mem_rev; rewrite -(eqP hxb). by move/roots_in/itvP->. move=> y; rewrite (itv_splitUeq hx) mem_rcons in_cons !andb_orl. have [->|_] := eqVneq y x; first by rewrite px0 orbT. by rewrite rxb rax in_nil !orbF. 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)