proposition: Lemma constructive_ivt (p : {poly R}) (a b : R) (eps : R) : a < b -> p.[a] < 0 -> 0 <= p.[b] -> 0 < eps -> { xy | let:(u,v):= xy in [&& pair_in_interval (- eps) (p.[u]) (p.[v]) eps, (pair_in_interval a u v b), (p.[u] < 0), (0 <= p.[v]) & (v - u) <= eps] }.
proof: Proof. move=> ab nla plb ep. move: (pol_ucont p (a:=a) (b:= b)); set c1 := _ .[_ ] => /= pc. set c := Num.max 1 c1. have lc1: 1 <= c by rewrite le_maxr lexx. have cpos:= (lt_le_trans ltr01 lc1). set k := Num.bound ((b - a) * c / eps). move: (upper_nthrootP(leqnn k)) => hh. exists (pol_approx p (a, b) k); move: (pol_approx_prop k nla plb ab). case:(pol_approx p (a, b) k) => u v /and4P [/eqP pa eq1 pun pvp]. case/and3P: (eq1) => [ha hb hc]. have c2p: 0 < v-u by rewrite subr_gt0. have hh1: (v-u) * c < eps. rewrite pa;set x := (X in _ / X). have xp: 0 < x by rewrite exprn_gt0 // ltr0n. rewrite mulrAC -(ltr_pmul2r xp) (mulrVK (unitf_gt0 xp)). move: hh. rewrite -/x. by rewrite ltr_pdivr_mulr// (mulrC _ x). have hh2 : v-u < eps. by apply: le_lt_trans hh1; rewrite - {1} (mulr1 (v-u)) (ler_pmul2l c2p). have dvp: p.[u] < p.[v] by apply (lt_le_trans pun pvp). have hh5: p.[v] - p.[u] <= eps. move: (pc _ _ ha (ltW hb) hc);rewrite gtr0_norm ? subr_gt0 // mulrC => hh4. apply:(le_trans _ (ltW hh1)); apply: (le_trans hh4). rewrite (ler_pmul2l c2p) le_maxr lexx orbT //. rewrite eq1 /pair_in_interval pun pvp dvp (ltW hh2) ler_oppl. rewrite (le_trans _ hh5) ?(le_trans _ hh5) //. by rewrite -{1} (addr0 p.[v]) ler_add2l oppr_ge0 ltW. by rewrite -{1} (add0r (- p.[u])) ler_add2r. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)