proposition: Lemma head_roots_on_ge p a b s : a < b -> roots_on p `]a, b[ s -> a < head b s.
proof: Proof. case: s => [|x s] ab // /(_ x). by rewrite in_cons eqxx; case/andP; case/andP. 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)