proposition: Lemma inf_of_continuous f a x (y := infimum BR_order (Zo BR (fun t => a <=r t /\ x <=r f t ))) : (forall t, realp t -> realp (f t)) -> (forall t, a <=r t -> continuous_at f t) -> (exists2 b, a <r b & x <=r f b) -> (a <r x) -> (f a <r x) -> a <r y /\ x = f y.
proof: Proof. move => fr fc fb xs fxs. rewrite /y; set A := Zo _ _; clear y. have xr:=(proj32_1 xs). have [or sr] := BR_osr. have ha: sub A BR by move => t /Zo_S. have hd: sub A (substrate BR_order) by ue. have hb: nonempty A. move: fb=> [b ba bb]; exists b; apply:Zo_i; first by exact:(proj32_1 ba). split => //; BRo_tac. have ar: realp a by exact:(proj31_1 xs). have hc1: inc a BR /\ (forall y, inc y A -> gle BR_order a y). split; [ exact | by move => t/Zo_P [_ [ /BR_gleP ]]]. have hc: bounded_below BR_order A by exists a; hnf; rewrite sr. move: (infimum_pr1 or (BR_inf_exists ha hb hc)). set y := (infimum BR_order A); move/(glbP or hd);rewrite /lower_bound. rewrite sr; move => [[yr sb] sc]. move: (sc _ hc1) => /BR_gleP lay. have lay': a <r y. split => // eay. move:(continuous_prop2 (fc _ (rleR ar)) fxs) => [e ea eb]. move/ rlt0xP:ea => ep; move:(BRsum_Mlegt0 lay ep) => le1. have er := (proj32_1 ep). have aer:=(RSs ar er). suff: a +r e <=r y by move: le1;rewrite eay => le1 le2;BRo_tac. apply/BR_gleP; apply:sc; split => // z /Zo_P [za [zb zc]]; apply/BR_gleP. case:(rleT_ee aer za) => // le2. suff: (BR_near a e z) by move/eb => le3; BRo_tac. apply/(BR_nearP _ ar er); split=> //. apply/(BRsum_le2r (RS_diff ar er) za er). rewrite BRsumC BRsum_diff //; exact:(proj1(BRsum_Mlegt0 zb ep)). split => //. have ysr := (fr _ yr). case: (rleT_ell xr ysr) => // le. move /(rlt_diffP xr ysr): (le) => ep. have ep1:=(BRhalf_pos ep). have [d dp de]:=(fc _ lay _ ep). have he: forall z, BR_near y d z -> x <=r f z. move => z /de [za zb]. apply/(rle_oppP xr za)/(rle_diffP1 (RSo za)(RSo xr)). rewrite -(BRdiff_sum_simpl_r (RSo xr)(RSo za) ysr) BRsumC (BRsumC _ (f y)). apply/(rle_diffP1 (RS_diff ysr za) (RS_diff ysr xr)). apply:(rleT (rle_abs (RS_diff ysr za)) zb). suff:(exists z, inc z A /\ z <r y) by move=> [z [/sb/BR_gleP za] zb]; BRo_tac. have dr:=(BRps_sBR dp). have le3:a <=r y +r d by exact:(proj1(rlt_ltT lay' (BRsum_Mps yr dp))). have le4: y -r d <r y by apply:(BRsum_Mms yr); apply:BRopp_positive1. case:(rleT_ee (RS_diff yr (BRps_sBR dp)) ar) => le2. exists a; split => //; apply/Zo_P; split => //; split; first by BRo_tac. by apply:he;apply/BR_nearP. move:(proj32 le2) => ydr. have lt4: x <=r f (y -r d). apply: he; split => //. by rewrite BRdiff_diff_simp // (BRabs_pos (BRps_sBRp dp)); apply: rleR. by exists (y -r d); split => //; apply/Zo_P. move: (continuous_prop2 (fc _ lay) le) => [e eps eb]. have er:= BRps_sBR eps. suff: gle BR_order (y +r e) y. move/BR_gleP;move:(BRsum_Mps yr eps) => la lb; BRo_tac. have yer: realp (y +r e) by apply:RSs. apply:sc; split => // z zA;apply/BR_gleP. move:(sb _ zA) => /BR_gleP lt1; move/Zo_P: zA => [zr [laz zc]]. case: (rleT_ee yer zr)=> // le2. have le3:= (BRms_sBRm (BRopp_positive1 eps)). have le4: y -r e <=r z by apply:(rleT (BRsum_Mm yr le3) lt1). have:(BR_near y e z) by apply/(BR_nearP _ yr er). move/eb => w; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)