proposition: Lemma Bolzano f x y: x <=r y -> Bolzano_hyp f x y -> f x <=r \0r -> \0r <=r f y -> exists2 z, (x <=r z /\ z <=r y) & f z = \0r.
proof: Proof. move => xy [Ha Hb Hc] la lb. set E1:= Zo BR (fun z => (x <=r z /\ z <=r y)). set E2:= Zo E1 (fun z => \0r <=r f z). have xr: realp x by BRo_tac. have yr: realp y by BRo_tac. have ha: sub E2 BR by move => t /Zo_S /Zo_S. move: BR_osr => [or sor]. have ye2: inc y E2 by apply:Zo_i => //; apply:Zo_i => //;split => //; BRo_tac. have hb: nonempty E2 by exists y. have hc1: lower_bound BR_order E2 x. split; first by rewrite sor. by move => t /Zo_S /Zo_P[ _ [ub uc]]; apply /BR_gleP. have hc: bounded_below BR_order E2 by exists x. have hd: sub E2 (substrate BR_order) by move => t /Zo_S /Zo_S; rewrite sor. move: (BR_inf_exists ha hb hc) => [z /(glbP or hd)]. rewrite /lower_bound sor; move => [[zr za] zb]. move: (za _ ye2) => /BR_gleP lzy. move:hc1; rewrite/lower_bound sor => /zb /BR_gleP lxz. have fzr: realp (f z). case: (equal_or_not x z) => ea; first by rewrite - ea; BRo_tac. case: (equal_or_not z y) => eb; first by rewrite eb; BRo_tac. apply:(continuous_real zr (Hc _ (conj lxz ea) (conj lzy eb))). case: (rleT_ell fzr RS0) => cp1. + by exists z. + case: (equal_or_not z y) => eb. move: lb; rewrite - eb => he; BRo_tac. have zyp: inc (y -r z) BRps by apply/ rlt0xP; apply/ rlt_diffP1. have [e ep ev]: exists2 e, inc e BRps & forall t, (BR_near z e t) -> z <r t -> f t <r \0r. case: (equal_or_not x z) => ea; last first. move: (continuous_prop2 (Hc _ (conj lxz ea) (conj lzy eb)) cp1). by move => [e ep eh]; exists e => // t ta _; apply: eh. move / rgt0xP: cp1; rewrite - ea => hb1. move:(BRhalf_neg hb1) => / rgt0xP hn. have ep: inc (BRopp (f x)) BRps by apply:BRopp_negative1. have hep:=(BRhalf_pos ep). have her:= (BRps_sBR hep). have fxr := (BRms_sBR hb1); have hfxr:=(RS_half fxr). move:(Ha _ hep) => [d dp dv]; ex_tac => t ta tb. move:(dv _ ta (proj1 tb)) => [ya yb]. move/ rlt0xP: hep => hep. move:(rle_abs (RS_diff ya fxr));rewrite (BRabs_diff ya fxr) => yc. move/(BRsum_le2r (proj31 yc) her fxr): (rleT yc yb). rewrite (BRsum_diff1 fxr ya); rewrite - {2} (BRdouble_half1 fxr). rewrite (BRhalf_opp fxr) BRsumC -/( _ -r _) BRdiff_sum // => he; BRo_tac. move:(rmin_prop2 ep zyp) (rmin_prop1 (BRps_sBR ep) (BRps_sBR zyp)). set t := (rmin e (y -r z)); move => tp [tr tb tc]. have te: z <r (z +r t) by exact: (BRsum_Mps zr tp). have td: (z +r t) <=r y. by move/(BRsum_le2l tr (RS_diff yr zr) zr): tc; rewrite (BRsum_diff zr yr). have tf: realp (z +r t) by apply:RSs. have tg: BR_near z e (z +r t). split => //. rewrite /BRdiff (BRoppD zr tr) (BRsumC (BRopp z)). by rewrite (BRsum_diff zr (RSo tr))(BRabs_opp tr)(BRabs_pos (BRps_sBRp tp)). have sa:= (ev _ tg te). have er:=(BRps_sBR ep). suff th:(forall u, inc u E2 -> gle BR_order (z +r t) u). move: (zb (z +r t) (conj tf th)) => /BR_gleP ti; BRo_tac. move => u /Zo_P [/Zo_P [ua [ub uc]] ud]; apply/BR_gleP. case: (rleT_el tf ua) => // ue. case: (rleT_ell zr ua) => uf. - move: cp1; rewrite uf => cp1; BRo_tac. - have zu: BR_near z e u. split => //; apply/(BRabs_prop3 zr ua er); split. move/(BRsum_le2r tr er zr): tb; rewrite BRsumC => th. move:(rleT (proj1 ue) th) => ti. move/(BRsum_le2r ua (proj32 ti) (RSo er)): ti. by rewrite -/( _ -r _) -/( _ -r _) BRdiff_sum. exact (proj1 (rlt_ltT uf (BRsum_Mps ua ep))). move:(ev _ zu uf) => ug; BRo_tac. - have te2: inc u E2 by apply:Zo_i => //; apply:Zo_i. move:(za _ te2) => /BR_gleP ug; BRo_tac. + case: (equal_or_not x z) => ea. by move: la; rewrite ea => he; BRo_tac. have zxp: inc (z -r x) BRps by apply/ rlt0xP; apply/ rlt_diffP1. have [e ep ev]: exists2 e, inc e BRps & forall t, (BR_near z e t) -> t <r z -> \0r <r f t. case: (equal_or_not z y) => eb. rewrite eb. have ep: inc (f z) BRps by apply/ rlt0xP. have hep:=(BRhalf_pos ep). have her:= (BRps_sBR hep). move:(Hb _ hep) => [d dp dv];ex_tac => t ta tb. move:(dv _ ta (proj1 tb)) => [ya yb]. move/ rlt0xP: hep => hep. move/ (BRabs_prop3 (proj32 lb) ya her): yb => [ _]. rewrite - eb - {1} (BRdouble_half1 (BRps_sBR ep)). move/(BRsum_le2r her ya her) => hc1; BRo_tac. move: (continuous_prop1 (Hc _ (conj lxz ea) (conj lzy eb)) cp1). by move => [e ep eh]; exists e => // t ta _; apply: eh. move:(rmin_prop2 ep zxp) (rmin_prop1 (BRps_sBR ep) (BRps_sBR zxp)). set t := (rmin e (z -r x)); move => tp [tr tb tc]. have td: x <=r (z -r t) by apply /(BRdiff_le2P zr tr xr). have te:= (BRsum_Mms zr (BRopp_positive1 tp)). have tf:= (proj31_1 te). have tg: BR_near z e (z -r t). split => //. by rewrite (BRdiff_diff zr zr tr) (BRdiff_xx zr) (BRsum_0l tr) (BRabs_poss). move:(ev _ tg te) => [th _]. have /za /BR_gleP /(rleNgt) //: inc (z -r t) E2. by apply:Zo_i => //; apply:Zo_i => //; split => //;apply:(rleT (proj1 te)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)