proposition: Lemma roots_on_rcons : forall p a b r s, sorted <%R (rcons s r) -> roots_on p `]a, b[ (rcons s r) -> roots_on p `]a, r[ s.
proof: Proof. move=> p a b r s; rewrite -{1}[s]revK -!rev_cons rev_sorted /=. move=> hrs /(@roots_on_same _ _ _ _ (r::s)) hr. have allrrs := order_path_min (rev_trans lt_trans) hrs. have allrs: all (< r) s. by apply/allP => x hx; apply: (allP allrrs); rewrite mem_rev. by case: (max_roots_on allrs (hr _))=> // x; rewrite mem_rcons. 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)