proposition: Lemma prev_root_in p a b : prev_root p a b \in `[minr a b, b].
proof: Proof. case: prev_rootP => [p0|y np0 py0 hy _|c np0 hc _]. * by rewrite bound_in_itv /<=%O /= le_minl lexx orbT. * by apply: subitvP hy; rewrite /<=%O /= /<=%O /= le_minl !lexx. * by rewrite hc bound_in_itv /<=%O /= le_minl lexx orbT. 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)