Skip to content

Commit

Permalink
for the CI with MC < 1.17
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist
affeldt-aist committed Oct 4, 2023
1 parent 6f93838 commit f29faa0
Showing 1 changed file with 53 additions and 55 deletions.
108 changes: 53 additions & 55 deletions theories/ereal.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -417,8 +417,8 @@ Qed.

Lemma lb_ereal_inf S M : lbound S M -> M <= ereal_inf S.
Proof.
move=> SM; rewrite /ereal_inf lee_oppr; apply ub_ereal_sup => x [y Sy <-{x}].
by rewrite lee_oppl oppeK; apply SM.
move=> SM; rewrite /ereal_inf lee_oppr; apply: ub_ereal_sup => x [y Sy <-{x}].
by rewrite lee_oppl oppeK; exact: SM.
Qed.

Lemma ub_ereal_sup_adherent S (e : R) : (0 < e)%R ->
Expand Down Expand Up @@ -479,7 +479,7 @@ have [|] := eqVneq (ubound U) set0.
rewrite -subset0 => U0; exists +oo.
split; [exact/ereal_ub_pinfty | apply/lbP => /= -[r0 /ubP Sr0|//|]].
- suff : ubound U r0 by move/U0.
by apply/ubP=> _ -[] [r1 Sr1 <-|//| /= _ <-]; rewrite -lee_fin; apply Sr0.
by apply/ubP=> _ -[] [r1 Sr1 <-|//| /= _ <-]; rewrite -lee_fin; apply: Sr0.
- by move/ereal_ub_ninfty => [|]; by [move/eqP : S0|move/eqP : Snoo].
set u : R := sup U.
exists u%:E; split; last first.
Expand All @@ -502,7 +502,7 @@ Lemma ereal_sup_ub S : ubound S (ereal_sup S).
Proof.
move=> y Sy; rewrite /ereal_sup /supremum ifF; last first.
by apply/eqP; rewrite predeqE => /(_ y)[+ _]; exact.
case: xgetP => /=; first by move=> _ -> -[] /ubP geS _; apply geS.
case: xgetP => /=; first by move=> _ -> -[] /ubP geS _; apply: geS.
by case: (ereal_supremums_neq0 S) => /= x0 Sx0; move/(_ x0).
Qed.

Expand All @@ -515,17 +515,17 @@ Qed.

Lemma ereal_inf_lb S : lbound S (ereal_inf S).
Proof.
by move=> x Sx; rewrite /ereal_inf lee_oppl; apply ereal_sup_ub; exists x.
by move=> x Sx; rewrite /ereal_inf lee_oppl; apply: ereal_sup_ub; exists x.
Qed.

Lemma ereal_inf_pinfty S : ereal_inf S = +oo <-> S `<=` [set +oo].
Proof. rewrite eqe_oppLRP oppe_subset image_set1; exact: ereal_sup_ninfty. Qed.

Lemma le_ereal_sup : {homo @ereal_sup R : A B / A `<=` B >-> A <= B}.
Proof. by move=> A B AB; apply ub_ereal_sup => x Ax; apply/ereal_sup_ub/AB. Qed.
Proof. by move=> A B AB; apply: ub_ereal_sup => x ?; apply/ereal_sup_ub/AB. Qed.

Lemma le_ereal_inf : {homo @ereal_inf R : A B / A `<=` B >-> B <= A}.
Proof. by move=> A B AB; apply lb_ereal_inf => x Bx; exact/ereal_inf_lb/AB. Qed.
Proof. by move=> A B AB; apply:lb_ereal_inf => x ?; exact/ereal_inf_lb/AB. Qed.

Lemma hasNub_ereal_sup (A : set (\bar R)) : ~ has_ubound A ->
A !=set0 -> ereal_sup A = +oo%E.
Expand Down Expand Up @@ -644,11 +644,9 @@ Global Instance ereal_dnbhs_filter :
Proof.
case=> [x||].
- case: (Proper_dnbhs_numFieldType x) => x0 [//= xT xI xS].
apply Build_ProperFilter' => //=; apply Build_Filter => //=.
move=> P Q lP lQ; exact: xI.
by move=> P Q PQ /xS; apply => y /PQ.
- apply Build_ProperFilter.
move=> P [x [xr xP]] //; exists (x + 1)%:E; apply xP => /=.
by apply: Build_ProperFilter' => //=; exact: Build_Filter.
- apply: Build_ProperFilter.
move=> P [x [xr xP]] //; exists (x + 1)%:E; apply: xP => /=.
by rewrite lte_fin ltr_addl.
split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]].
+ by exists 0%R.
Expand All @@ -658,11 +656,11 @@ case=> [x||].
[apply/gtMP; rewrite MP0 | apply/gtMQ; rewrite MQ0].
exists `|MQ|%R; rewrite realE normr_ge0; split => // x MQx; split.
by apply: gtMP; rewrite (le_lt_trans _ MQx) // MP0 lee_fin.
by apply gtMQ; rewrite (le_lt_trans _ MQx)// lee_fin real_ler_normr ?lexx.
by apply: gtMQ; rewrite (le_lt_trans _ MQx)// lee_fin real_ler_normr ?lexx.
have [MQ0|MQ0] := eqVneq MQ 0%R.
exists `|MP|%R; rewrite realE normr_ge0; split => // x MPx; split.
by apply gtMP; rewrite (le_lt_trans _ MPx)// lee_fin real_ler_normr ?lexx.
by apply gtMQ; rewrite (le_lt_trans _ MPx) // lee_fin MQ0.
by apply: gtMP; rewrite (le_lt_trans _ MPx)// lee_fin real_ler_normr ?lexx.
by apply: gtMQ; rewrite (le_lt_trans _ MPx) // lee_fin MQ0.
have {}MP0 : (0 < `|MP|)%R by rewrite normr_gt0.
have {}MQ0 : (0 < `|MQ|)%R by rewrite normr_gt0.
exists (Num.max (PosNum MP0) (PosNum MQ0))%:num.
Expand All @@ -673,7 +671,7 @@ case=> [x||].
by apply/gtMQ; rewrite lte_fin (le_lt_trans _ MQx)// real_ler_normr ?lexx.
* by move=> _; split; [apply/gtMP | apply/gtMQ].
+ by exists M; split => // ? /gtM /sPQ.
- apply Build_ProperFilter.
- apply: Build_ProperFilter.
+ move=> P [M [Mr ltMP]]; exists (M - 1)%:E.
by apply: ltMP; rewrite lte_fin gtr_addl oppr_lt0.
+ split=> /= [|P Q [MP [MPr ltMP]] [MQ [MQr ltMQ]] |P Q sPQ [M [Mr ltM]]].
Expand All @@ -684,15 +682,15 @@ case=> [x||].
[apply/ltMP; rewrite MP0 | apply/ltMQ; rewrite MQ0].
exists (- `|MQ|)%R; rewrite realN realE normr_ge0; split => // x xMQ.
split.
by apply ltMP; rewrite (lt_le_trans xMQ)// lee_fin MP0 ler_oppl oppr0.
apply ltMQ; rewrite (lt_le_trans xMQ) // lee_fin ler_oppl -normrN.
by apply: ltMP; rewrite (lt_le_trans xMQ)// lee_fin MP0 ler_oppl oppr0.
apply: ltMQ; rewrite (lt_le_trans xMQ) // lee_fin ler_oppl -normrN.
by rewrite real_ler_normr ?realN // lexx.
* have [MQ0|MQ0] := eqVneq MQ 0%R.
exists (- `|MP|)%R; rewrite realN realE normr_ge0; split => // x MPx.
split.
apply ltMP; rewrite (lt_le_trans MPx) // lee_fin ler_oppl -normrN.
apply: ltMP; rewrite (lt_le_trans MPx) // lee_fin ler_oppl -normrN.
by rewrite real_ler_normr ?realN // lexx.
by apply ltMQ; rewrite (lt_le_trans MPx) // lee_fin MQ0 ler_oppl oppr0.
by apply: ltMQ; rewrite (lt_le_trans MPx) // lee_fin MQ0 ler_oppl oppr0.
have {}MP0 : (0 < `|MP|)%R by rewrite normr_gt0.
have {}MQ0 : (0 < `|MQ|)%R by rewrite normr_gt0.
exists (- (Num.max (PosNum MP0) (PosNum MQ0))%:num)%R.
Expand Down Expand Up @@ -863,9 +861,9 @@ Proof.
apply/propeqP; split; first by apply: filterS => ?; apply: nbhs_singleton.
move=> [M [Mreal AM]]; near=> k; near=> x; apply: AM.
apply: (@lt_trans _ _ (k - 1)%R).
by rewrite ltrBrDl; near: k; apply: nbhs_pinfty_gt; rewrite realD.
by rewrite ltr_subr_addl; near: k; apply: nbhs_pinfty_gt; rewrite realD.
have kreal : k \is Num.real by near: k; apply: nbhs_pinfty_real.
by apply: ltr_distlBl; near: x; apply: nbhsx_ballx.
by apply: ltr_distl_subl; near: x; apply: nbhsx_ballx.
Unshelve. all: by end_near. Qed.

Lemma nearNy_join (A : set R) :
Expand All @@ -874,9 +872,9 @@ Proof.
apply/propeqP; split; first by apply: filterS => ?; apply: nbhs_singleton.
move=> [M [Mreal AM]]; near=> k; near=> x; apply: AM.
apply: (@lt_trans _ _ (k + 1)%R); last first.
by rewrite -ltrBrDr; near: k; apply: nbhs_ninfty_lt; rewrite realB.
by rewrite -ltr_subr_addr; near: k; apply: nbhs_ninfty_lt; rewrite realB.
have kreal : k \is Num.real by near: k; apply: nbhs_ninfty_real.
by rewrite ltr_distlDr// distrC; near: x; apply: nbhsx_ballx.
by rewrite ltr_distl_addr// distrC; near: x; apply: nbhsx_ballx.
Unshelve. all: by end_near. Qed.

Lemma ereal_nbhs_nbhs (p : \bar R) (A : set (\bar R)) :
Expand Down Expand Up @@ -908,28 +906,28 @@ case: x => [r /=| |].
rewrite predeqE => S; split => [[_/posnumP[e] reS]|[S' [_ /posnumP[e] reS' <-]]].
exists (-%E @` S).
exists e%:num => //= r1 rer1; exists (- r1%:E); last by rewrite oppeK.
by apply reS; rewrite /ball /= opprK -normrN opprD opprK.
by apply: reS; rewrite /ball /= opprK -normrN opprD opprK.
rewrite predeqE => s; split => [[y [z Sz] <- <-]|Ss].
by rewrite oppeK.
by exists (- s); [exists s | rewrite oppeK].
exists e%:num => //= r1 rer1; exists (- r1%:E); last by rewrite oppeK.
by apply reS'; rewrite /ball /= opprK -normrN opprD.
by apply: reS'; rewrite /ball /= opprK -normrN opprD.
- rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]].
exists (-%E @` S).
exists (- M)%R; rewrite realN Mreal; split => // x Mx.
by exists (- x); [apply MS; rewrite lte_oppl | rewrite oppeK].
by exists (- x); [apply: MS; rewrite lte_oppl | rewrite oppeK].
rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK.
by exists (- x); [exists x | rewrite oppeK].
exists (- M)%R; rewrite realN; split => // y yM.
exists (- y); by [apply Mx; rewrite lte_oppr|rewrite oppeK].
exists (- y); by [apply: Mx; rewrite lte_oppr|rewrite oppeK].
- rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]].
exists (-%E @` S).
exists (- M)%R; rewrite realN Mreal; split => // x Mx.
by exists (- x); [apply MS; rewrite lte_oppr | rewrite oppeK].
by exists (- x); [apply: MS; rewrite lte_oppr | rewrite oppeK].
rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK.
by exists (- x); [exists x | rewrite oppeK].
exists (- M)%R; rewrite realN; split => // y yM.
exists (- y); by [apply Mx; rewrite lte_oppl|rewrite oppeK].
exists (- y); by [apply: Mx; rewrite lte_oppl|rewrite oppeK].
Qed.

Lemma nbhsNKe (R : realFieldType) (z : \bar R) (A : set (\bar R)) :
Expand All @@ -951,7 +949,7 @@ Qed.

Lemma oppe_continuous (R : realFieldType) : continuous (@oppe R).
Proof.
move=> x S /= xS; apply nbhsNKe; rewrite image_preimage //.
move=> x S /= xS; apply: nbhsNKe; rewrite image_preimage //.
by rewrite predeqE => y; split => // _; exists (- y) => //; rewrite oppeK.
Qed.

Expand Down Expand Up @@ -1005,34 +1003,34 @@ Let contract := @contract R.
Lemma sup_contract_le1 S : S !=set0 -> (`|sup (contract @` S)| <= 1)%R.
Proof.
case=> x Sx; rewrite ler_norml; apply/andP; split; last first.
apply sup_le_ub; first by exists (contract x), x.
apply: sup_le_ub; first by exists (contract x), x.
by move=> r [y Sy] <-; case/ler_normlP : (contract_le1 y).
rewrite (@le_trans _ _ (contract x)) //.
by case/ler_normlP : (contract_le1 x); rewrite ler_oppl.
apply sup_ub; last by exists x.
apply: sup_ub; last by exists x.
by exists 1%R => r [y Sy <-]; case/ler_normlP : (contract_le1 y).
Qed.

Lemma contract_sup S : S !=set0 -> contract (ereal_sup S) = sup (contract @` S).
Proof.
move=> S0; apply/eqP; rewrite eq_le; apply/andP; split; last first.
apply sup_le_ub.
apply: sup_le_ub.
by case: S0 => x Sx; exists (contract x), x.
move=> x [y Sy] <-{x}; rewrite le_contract; exact/ereal_sup_ub.
rewrite leNgt; apply/negP.
set supc := sup _; set csup := contract _; move=> ltsup.
suff [y [ysupS ?]] : exists y, y < ereal_sup S /\ ubound S y.
have : ereal_sup S <= y by apply ub_ereal_sup.
have : ereal_sup S <= y by exact: ub_ereal_sup.
by move/(lt_le_trans ysupS); rewrite ltxx.
suff [x [? [ubSx x1]]] : exists x, (x < csup)%R /\ ubound (contract @` S) x /\
(`|x| <= 1)%R.
exists (expand x); split => [|y Sy].
by rewrite -(contractK (ereal_sup S)) lt_expand // inE // contract_le1.
by rewrite -(contractK y) le_expand //; apply ubSx; exists y.
by rewrite -(contractK y) le_expand //; apply: ubSx; exists y.
exists ((supc + csup) / 2); split; first by rewrite midf_lt.
split => [r [y Sy <-{r}]|].
rewrite (@le_trans _ _ supc) ?midf_le //; last by rewrite ltW.
apply sup_ub; last by exists y.
apply: sup_ub; last by exists y.
by exists 1%R => r [z Sz <-]; case/ler_normlP : (contract_le1 z).
rewrite ler_norml; apply/andP; split; last first.
rewrite ler_pdivr_mulr // mul1r (_ : 2 = 1 + 1)%R // ler_add //.
Expand Down Expand Up @@ -1143,7 +1141,7 @@ move=> e1 reA; suff h : nbhs +oo (-%E @` A).
rewrite (_ : -oo = - +oo) // nbhsNe; exists (-%E @` A) => //.
rewrite predeqE => x; split=> [[y [z Az <- <-]]|Ax]; rewrite ?oppeK //.
by exists (- x); [exists x | rewrite oppeK].
apply (@nbhs_oo_up_e1 _ e) => // x x1e; exists (- x); last by rewrite oppeK.
apply: (@nbhs_oo_up_e1 _ e) => // x x1e; exists (- x); last by rewrite oppeK.
by apply/reA/ereal_ballN; rewrite oppeK.
Qed.

Expand All @@ -1152,11 +1150,11 @@ Lemma nbhs_oo_up_1e (A : set (\bar R)) (e : {posnum R}) : (1 < e%:num)%R ->
Proof.
move=> e1 reA; have [e2{e1}|e2] := ltrP 2 e%:num.
suff -> : A = setT by exists 0%R.
rewrite predeqE => x; split => // _; apply reA.
rewrite predeqE => x; split => // _; apply: reA.
exact/ereal_ballN/ereal_ball_ninfty_oversize.
have /andP[e10 e11] : (0 < e%:num - 1 <= 1)%R.
by rewrite subr_gt0 e1 /= ler_subl_addl.
apply nbhsNKe.
apply: nbhsNKe.
have : ((PosNum e10)%:num <= 1)%R by [].
move/(@nbhs_oo_down_e1 (-%E @` A) (PosNum e10)); apply.
move=> y ye; exists (- y); last by rewrite oppeK.
Expand All @@ -1172,7 +1170,7 @@ move=> e1 reA; have [e2{e1}|e2] := ltrP 2 e%:num.
by rewrite predeqE => x; split => // _; exact/reA/ereal_ball_ninfty_oversize.
have /andP[e10 e11] : (0 < e%:num - 1 <= 1)%R.
by rewrite subr_gt0 e1 /= ler_subl_addl.
apply nbhsNKe.
apply:nbhsNKe.
have : ((PosNum e10)%:num <= 1)%R by [].
move/(@nbhs_oo_up_e1 (-%E @` A) (PosNum e10)); apply.
move=> y ye; exists (- y); last by rewrite oppeK.
Expand All @@ -1195,7 +1193,7 @@ have e'0 : (0 < e')%R.
rewrite subr_gt0 -lte_fin -[ltRHS](contractK r%:E).
rewrite fine_expand // lt_expand ?inE ?contract_le1// ?ltW//.
by rewrite ltr_subl_addl ltr_addr.
apply/nbhs_ballP; exists e' => // r' re'r'; apply reA.
apply/nbhs_ballP; exists e' => // r' re'r'; apply: reA.
by have [?|?] := lerP r r';
[exact: contract_ereal_ball_fin_le | exact: ball_ereal_ball_fin_lt].
Qed.
Expand All @@ -1214,7 +1212,7 @@ pose e' : R := (fine (expand (contract r%:E + e%:num)) - r)%R.
have e'0 : (0 < e')%R.
rewrite /e' subr_gt0 -lte_fin -[in ltLHS](contractK r%:E).
by rewrite fine_expand // lt_expand ?inE ?contract_le1 ?ltr_addl ?ltW.
apply/nbhs_ballP; exists e' => // r' r'e'r; apply reA.
apply/nbhs_ballP; exists e' => // r' r'e'r; apply: reA.
by have [?|?] := lerP r r';
[exact: ball_ereal_ball_fin_le | exact: contract_ereal_ball_fin_lt].
Qed.
Expand All @@ -1226,11 +1224,11 @@ Lemma nbhs_fin_out_above_below r (e : {posnum R}) (A : set (\bar R)) :
nbhs r%:E A.
Proof.
move=> reA reN1 re1; suff : A = setT by move->; apply: filterT.
rewrite predeqE => x; split => // _; apply reA.
rewrite predeqE => x; split => // _; apply: reA.
case: x => [r'| |] //.
- have [?|?] := lerP r r'.
+ by apply: contract_ereal_ball_fin_le => //; exact/ltW.
+ by apply contract_ereal_ball_fin_lt => //; exact/ltW.
+ by apply: contract_ereal_ball_fin_lt => //; exact/ltW.
- exact/contract_ereal_ball_pinfty.
- apply/ereal_ballN/contract_ereal_ball_pinfty.
by rewrite EFinN contractN -(opprK 1%R) ltr_oppl opprD opprK.
Expand All @@ -1247,15 +1245,15 @@ have [|reN1] := boolP (contract r%:E - e%:num == -1)%R.
rewrite opprK -mulr2n mulrn_eq0 orFb contract_eq0 => /eqP[r0].
move: re1; rewrite r0 contract0 add0r => /eqP e1.
apply/nbhs_ballP; exists 1%R => //= r'; rewrite /ball /= sub0r normrN => r'1.
apply reA.
apply: reA.
by rewrite /ereal_ball r0 contract0 sub0r normrN e1 contract_lt1.
rewrite neq_lt => /orP[re1|re1].
by apply (@nbhs_fin_out_below _ e) => //; rewrite reN1 addrAC subrr sub0r.
by apply: (@nbhs_fin_out_below _ e) => //; rewrite reN1 addrAC subrr sub0r.
have e1 : (1 < e%:num)%R.
move: re1; rewrite reN1 addrAC ltr_subr_addl -!mulr2n -(mulr_natl e%:num).
by rewrite -{1}(mulr1 2%:R) => ?; rewrite -(@ltr_pmul2l _ 2).
have Aoo : setT `\ -oo `<=` A.
move=> x [_]; rewrite /set1 /= => xnoo; apply reA.
move=> x [_]; rewrite /set1 /= => xnoo; apply: reA.
case: x xnoo => [r' _ | _ |//].
have [rr'|r'r] := lerP (contract r%:E) (contract r'%:E).
apply: contract_ereal_ball_fin_le; last exact/ltW.
Expand All @@ -1270,7 +1268,7 @@ have [|reN1] := boolP (contract r%:E - e%:num == -1)%R.
by apply/nbhs_ballP; exists e'%:num => //= y /h; apply: Aoo.
move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1].
have [re1|re1] := eqVneq (contract r%:E + e%:num)%R 1%R.
by apply (@nbhs_fin_out_above _ e) => //; rewrite re1.
by apply: (@nbhs_fin_out_above _ e) => //; rewrite re1.
move: re1; rewrite neq_lt => /orP[re1|re1].
have ? : (`|contract r%:E - e%:num| < 1)%R.
rewrite ltr_norml reN1 andTb ltr_subl_addl.
Expand All @@ -1289,15 +1287,15 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1].
by rewrite ltr_subl_addl ltr_addr.
rewrite subr_gt0 -lte_fin -[in ltLHS](contractK r%:E).
by rewrite fine_expand// lt_expand ?inE ?contract_le1 ?ltr_addl ?ltW.
apply/nbhs_ballP; exists e' => // r' re'r'; apply reA.
apply/nbhs_ballP; exists e' => // r' re'r'; apply: reA.
have [|r'r] := lerP r r'.
move=> rr'; apply: ball_ereal_ball_fin_le => //.
by apply: le_ball re'r'; rewrite le_minl lexx orbT.
move: re'r'; rewrite /ball /= lt_minr => /andP[].
rewrite gtr0_norm ?subr_gt0 // -ltr_subl_addl addrAC subrr add0r ltr_oppl.
rewrite opprK -lte_fin fine_expand // => r'e'r _.
exact: expand_ereal_ball_fin_lt.
by apply (@nbhs_fin_out_above _ e) => //; rewrite ltW.
by apply: (@nbhs_fin_out_above _ e) => //; rewrite ltW.
have [re1|re1] := ltrP 1 (contract r%:E + e%:num).
exact: (@nbhs_fin_out_above_below _ e).
move: re1; rewrite le_eqVlt => /orP[re1|re1].
Expand All @@ -1309,7 +1307,7 @@ move: re1; rewrite le_eqVlt => /orP[re1|re1].
rewrite -(mulr_natl e%:num) -{1}(mulr1 2%:R) => ?.
by rewrite -(@ltr_pmul2l _ 2).
have Aoo : (setT `\ +oo `<=` A).
move=> x [_]; rewrite /set1 /= => xpoo; apply reA.
move=> x [_]; rewrite /set1 /= => xpoo; apply: reA.
case: x xpoo => [r' _ | // |_].
rewrite /ereal_ball.
have [rr'|r'r] := lerP (contract r%:E) (contract r'%:E).
Expand All @@ -1326,7 +1324,7 @@ move: re1; rewrite le_eqVlt => /orP[re1|re1].
have : nbhs r%:E (setT `\ +oo) by exists 1%R => /=.
case => _/posnumP[x] /=; rewrite /ball_ => h.
by exists x%:num => //= y /h; exact: Aoo.
by apply (@nbhs_fin_out_below _ e) => //; rewrite ltW.
by apply: (@nbhs_fin_out_below _ e) => //; rewrite ltW.
Qed.

Lemma ereal_nbhsE : nbhs = nbhs_ (entourage_ (@ereal_ball R)).
Expand Down Expand Up @@ -1415,7 +1413,7 @@ rewrite predeq2E => x A; split.
by move: (contract_lt1 M); rewrite ltr_norml => /andP[].
case=> [r| |].
* rewrite /ereal_ball => /= rM1.
apply MA.
apply: MA.
rewrite lte_fin.
rewrite ler0_norm in rM1; last first.
rewrite ler_subl_addl addr0 ltW //.
Expand All @@ -1431,7 +1429,7 @@ rewrite predeq2E => x A; split.
* rewrite /ereal_ball /= => _; exact: MA.
- case: x => [r [E [_/posnumP[e] reA] sEA] | [E [_/posnumP[e] reA] sEA] |
[E [_/posnumP[e] reA] sEA]] //=.
+ by apply nbhs_fin_inbound with e => ? ?; exact/sEA/reA.
+ by apply: (@nbhs_fin_inbound _ e) => ? ?; exact/sEA/reA.
+ have [|] := boolP (e%:num <= 1)%R.
by move/nbhs_oo_up_e1; apply => ? ?; exact/sEA/reA.
by rewrite -ltNge => /nbhs_oo_up_1e; apply => ? ?; exact/sEA/reA.
Expand Down

0 comments on commit f29faa0

Please sign in to comment.