proposition: Lemma head_roots_ge : forall p a b, a < b -> a < head b (roots p a b).
proof: Proof. by move=> p a b; case: rootsP=> // *; apply: head_roots_on_ge. 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)