proposition: Lemma constructive_ivt_ter (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. have ba' : 0 < b - a by rewrite -(addrN a) ltr_add2r. have evalba : 0 < p.[b] - p.[a] by rewrite subr_gt0; exact: lt_le_trans plb. move: (pol_ucont p (a:=a) (b:= b)). set c := _ .[_ ] => /= pc. have cpos : 0 < c. rewrite - (ltr_pmul2r ba') mul0r. by apply: lt_le_trans (pc a b _ _ _) => //; rewrite ? ger0_norm // ltW. have pdiv : (0 < (b - a) * c / eps) by rewrite ltr_pdivl_mulr // mul0r mulr_gt0. move: (archi_boundP (ltW pdiv)); set n := Num.bound _ => qn. have fact1 : (0 : R) < n%:R by exact: lt_trans qn => /=. case: n qn fact1 => [|n]; rewrite ?ltxx // => qn _. pose sl := map (fun x => a + (b - a) * (x%:R / (n.+1%:R))) (iota 0 n.+2). pose a'_index := find (fun x => p.[x] >= 0) sl. have has_sl : has (fun x => p.[x] >= 0) sl. rewrite has_map; apply/hasP; exists n.+1. by rewrite mem_iota add0n ltnSn ltnW. by rewrite /= divff ? pnatr_eq0 // mulr1 addrCA subrr addr0. case: {2}a'_index (refl_equal a'_index) => [|ia']. rewrite /a'_index => ha'; have:= (nth_find 1 has_sl); rewrite ha' /=. by rewrite mul0r mulr0 addr0 leNgt nla. set b':= sl`_ia'.+1; set a' := sl`_ia'. move=> ha'; exists (a', b'); simpl. have ia's : (ia' < size sl)%N by rewrite -ha' /a'_index find_size. have ia'iota : (ia' < size (iota 0 n.+2))%N by move: ia's; rewrite size_map. have:= (nth_find 0 has_sl); rewrite -/a'_index ha' => pb'p. have:= (ltnSn ia'); rewrite -{2}ha'. move/(@before_find _ 0 (fun x : R => 0 <= p.[x]) sl); move/negbT. rewrite -ltNge => pa'n. move:(ltW ba') => ba'w. have aa' : a <= a'. rewrite /a'/sl (nth_map 0%N) // ler_addl mulr_ge0 //. by rewrite mulr_ge0 // ?invr_ge0 ?ler0n. have ia'_sharp : (ia' < n.+1)%N. move: ia'iota; rewrite leq_eqVlt; rewrite size_iota; case/orP=> //. move/eqP; case=> abs. move: pa'n; rewrite abs (nth_map 0%N) ?size_iota // nth_iota //. rewrite add0n divff ?mulr1 ?pnatr_eq0 // addrCA subrr addr0 => {} abs. by move: plb; rewrite leNgt abs. have b'b : b' <= b. rewrite /b'/sl (nth_map 0%N) ?size_iota ?ltnS // nth_iota // add0n. have e : b = a + (b - a) by rewrite addrCA subrr addr0. rewrite {2}e {e} ler_add2l //= -{2}(mulr1 (b -a)) ler_wpmul2l //. rewrite ler_pdivr_mulr ?ltr0Sn // mul1r -subr_gte0 /=. have -> : (n.+1 = ia'.+1 + (n.+1 - ia'.+1))%N by rewrite subnKC. by rewrite mulrnDr addrAC subrr add0r subSS ler0n. have b'a'_sub : b' - a' = (b - a) / (n.+1)%:R. have side : (ia' < n.+2)%N by apply: ltn_trans (ltnSn _). rewrite /b' /a' /sl (nth_map 0%N) ?size_iota // nth_iota // add0n. rewrite (nth_map 0%N) ?size_iota // nth_iota // add0n. rewrite opprD addrAC addrA subrr add0r addrC -mulrBr. by congr (_ * _); rewrite -mulrBl mulrSr addrAC subrr add0r div1r. have a'b' : a' < b'. move/eqP: b'a'_sub; rewrite subr_eq; move/eqP->; rewrite ltr_addr. by rewrite mulr_gt0 // invr_gt0 ltr0Sn. rewrite pa'n a'b' b'b aa' pb'p. have : `|p.[b'] - p.[a']| <= eps. have := (pc sl`_ia' sl`_ia'.+1 aa' (ltW a'b') b'b). rewrite b'a'_sub => hpc; apply: le_trans hpc _ => /=. rewrite mulrA ler_pdivr_mulr ?ltr0Sn // mulrC [eps * _]mulrC. rewrite -ler_pdivr_mulr //; apply: (ltW qn). case/ler_normlP => h1 h2. rewrite ler_oppl -(ler_add2l p.[b']) (le_trans h2) ? ler_addr //. by rewrite -(ler_add2r (- p.[a'])) (le_trans h2) // ler_addl oppr_gte0 ltW. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)