proposition: Lemma weak_ivt (p : {poly F}) (a b : F) : a <= b -> p.[a] <= 0 <= p.[b] -> { x : alg | a%:RA <= x <= b%:RA & root (p ^ to_alg) x }.
proof: Proof. move=> le_ab; have [-> _|p_neq0] := eqVneq p 0. by exists a%:RA; rewrite ?lexx ?ler_to_alg // rmorph0 root0. move=> /andP[pa_le0 pb_ge0]; apply/sig2W. have hpab: p.[a] * p.[b] <= 0 by rewrite mulr_le0_ge0. move=> {pa_le0 pb_ge0}; wlog monic_p : p hpab p_neq0 / p \is monic. set q := (lead_coef p) ^-1 *: p => /(_ q). rewrite !hornerZ mulrCA !mulrA -mulrA mulr_ge0_le0 //; last first. by rewrite (@exprn_even_ge0 _ 2). have mq: q \is monic by rewrite monicE lead_coefZ mulVf ?lead_coef_eq0. rewrite monic_neq0 ?mq=> // [] [] // x hx hqx; exists x=> //. move: hqx; rewrite /q -mul_polyC rmorphM /= rootM map_polyC rootC. by rewrite fmorph_eq0 invr_eq0 lead_coef_eq0 (negPf p_neq0). pose c := (a + b) / 2%:R; pose r := (b - a) / 2%:R. have r_ge0 : 0 <= r by rewrite mulr_ge0 ?ger0E // subr_ge0. have hab: ((c - r = a)%R * (c + r = b)%R)%type. rewrite -mulrDl -mulrBl opprD addrA addrK opprK. rewrite addrAC addrA [a + _ + _]addrAC subrr add0r. by rewrite !mulrDl -![_ + _](splitf 2). have hp: p.[c - r] * p.[c + r] <= 0 by rewrite !hab. pose x := AlgDom monic_p r_ge0 hp; exists (\pi_alg (to_algcreal x)). rewrite !piE; apply/andP; rewrite -!(rwP le_algP) /=. split; by do [ unlock to_algcreal=> /=; apply: (@le_crealP _ 0%N)=> /= j _; have := @to_algcreal_ofP p c r 0%N j r_ge0 isT; rewrite ler_distl /= expr0 divr1 !hab=> /andP []]. apply/rootP; rewrite horner_pi zeroE -equiv_alg horner_algcrealE /=. by rewrite -(@to_algcrealP x); unlock to_algcreal. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial generic_quotient) mathcomp(cauchyreals separable zmodp bigenough)