proposition: Lemma last_roots_on_le p a b s : a < b -> roots_on p `]a, b[ s -> last a s < b.
proof: Proof. case: s => [|x s] ab rs //. by rewrite (itvP (roots_on_in rs _)) //= mem_last. 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)