proposition: Lemma Bolzano2 f x y v: x <=r y -> Bolzano_hyp f x y -> (BR_between v (f x) (f y)) -> exists2 z, (x <=r z /\ z <=r y) & f z = v.
proof: Proof. move => lexy; move: f v. suff:forall f v, Bolzano_hyp f x y -> ((f x) <=r v /\ v <=r (f y)) -> exists2 z, x <=r z /\ z <=r y & f z = v. move => H f v Ha; case;first by apply:H. move => [ha hb]. pose g z := BRopp (f z). have hc: g x <=r (BRopp v) /\ (BRopp v) <=r g y by split; apply :rle_opp. move: Ha => [H1 H2 H3]. move: (ha) => [fyr vr _]. have H1': continuous_right g x. move => e ep; move: (H1 e ep) => [d dp dv]; ex_tac => z za zb. move:(dv _ za zb) => [hu uv]; rewrite /g; split; first by apply:RSo. rewrite /BRdiff (BRopp_K hu) BRsumC. by move: uv; rewrite (BRabs_diff (proj32 hb) hu). have H2': continuous_left g y. move => e ep; move: (H2 e ep) => [d dp dv]; ex_tac => z za zb. move:(dv _ za zb) => [hu uv]; rewrite /g; split; first by apply:RSo. rewrite /BRdiff (BRopp_K hu) BRsumC. by move: uv; rewrite (BRabs_diff fyr hu). have H3': forall z, x <r z -> z <r y -> continuous_at g z. move => z za zb; move: (H3 _ za zb) => h1. apply:(continuous_comp(H3 _ za zb));apply:continuous_opp. apply:(continuous_real (proj32_1 za) h1). have hd: Bolzano_hyp g x y by split. move:(H _ _ hd hc) => [z za zb];exists z => //;apply BRopp_inj => //. case:(equal_or_not x z) => lxz; first by rewrite - lxz; exact (proj32 hb). case:(equal_or_not z y) => lzy; first by rewrite lzy. move: (H3 _ (conj (proj1 za) lxz) (conj (proj2 za) lzy)). by move/ (continuous_real (proj32 (proj1 za)) ). move => f v [Ha Hb Hc] [fxv fyv]. move: (fxv) => [fxr vr _]. move:(RSo vr) => ovr. pose g z := f z +r (BRopp v). have Ha': continuous_right g x. move => e ep; move:(Ha e ep) => [d dp dv]; exists d => // z za zb. move:(dv _ za zb) => [zc zd]; split; first by apply:RSs. by rewrite /g BRdiff_sum_simpl_r. have Hb': continuous_left g y. move => e ep; move:(Hb e ep) => [d dp dv]; exists d => // z za zb. move:(dv _ za zb) => [zc zd]; split; first by apply:RSs. rewrite /g BRdiff_sum_simpl_r => //; BRo_tac. have H': Bolzano_hyp g x y. split => // z za zb; move:(Hc _ za zb) => cc. rewrite /g. move:(proj2 (continuous2_sum (continuous_real (proj32_1 za) cc) ovr)) => h. exact:(continuous_comp cc h). have ha: g x <=r \0r. move/(BRsum_le2r (proj31 fxv) (proj32 fxv) ovr): fxv. by rewrite BRsum_opp_r. have hb: \0r <=r g y by move/(rle_diffP1 vr (proj32 fyv)): fyv. move: (Bolzano lexy H' ha hb) => [z [za zb] zc]; exists z => //. apply:BRdiff_xx_rw => //. case: (equal_or_not x z) => exz; first by ue. case: (equal_or_not z y) => ezy; first by rewrite ezy; BRo_tac. exact:(continuous_real (proj32 za) (Hc _ (conj za exz) (conj zb ezy))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)