proposition: Lemma constructive_ivt_bis (p : {poly R})(a b : R) (eps: R): a < b -> p.[a] < 0 -> 0 <= p.[b] -> 0 < eps -> { xy | (- eps <= p.[xy.1]) && (p.[xy.1] < 0) && (0 <= p.[xy.2]) && (p.[xy.2] <= eps) && (a <= xy.1) && (xy.1 < xy.2) && (xy.2 <= b) }.
proof: Proof. move=> ab nla plb ep. move:(constructive_ivt ab nla plb ep) => [xy etc]. exists xy. set u := xy.1; set v := xy.2; move: etc. have ->: xy = (u,v) by rewrite /u /v; case xy. by case/and5P => [/and3P[-> _ ->] /and3P[-> -> ->] -> -> _]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)