proposition: Lemma rootsEba p a b : b <= a -> roots p a b = [::].
proof: Proof. case: rootsP=> // p0; case: (roots _ _ _) => [|x s] hs ps ba //; by move: (hs x); rewrite itv_ge -?leNgt //= mem_head. 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)