proposition: Lemma nbhs_fin_inbound r (e : {posnum R}) (A : set (\bar R)) : ereal_ball r%:E e%:num `<=` A -> nbhs r%:E A.
proof: Proof. move=> reA. have [|reN1] := boolP (contract r%:E - e%:num == -1)%R. rewrite subr_eq addrC => /eqP reN1. have [re1|] := boolP (contract r%:E + e%:num == 1)%R. move/eqP : reN1; rewrite -(eqP re1) opprD addrCA subrr addr0 -subr_eq0. 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. 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. have e1 : (1 < e%:num)%R. move: re1; rewrite reN1 addrAC ltrBrDl -!mulr2n -(mulr_natl e%:num). by rewrite -{1}(mulr1 2%:R) => ?; rewrite -(@ltr_pM2l _ 2). have Aoo : setT `\ -oo `<=` A. 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. by rewrite -lee_fin -(contractK r%:E) -(contractK r'%:E) le_expand. apply: contract_ereal_ball_fin_lt; last first. by rewrite reN1 addrAC subrr add0r. rewrite -lte_fin -(contractK r%:E) -(contractK r'%:E). by rewrite lt_expand // inE; exact: contract_le1. exact: contract_ereal_ball_pinfty. have : nbhs r%:E (setT `\ -oo) by apply/nbhs_ballP; exists 1%R => /=. move=> /nbhs_ballP[_/posnumP[e']] /=; rewrite /ball /= => h. 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. move: re1; rewrite neq_lt => /orP[re1|re1]. have ? : (`|contract r%:E - e%:num| < 1)%R. rewrite ltr_norml reN1 andTb ltrBlDl. rewrite (@lt_le_trans _ _ 1%R) // ?lerDr//. by case/ltr_normlP : (contract_lt1 r). have ? : (`|contract r%:E + e%:num| < 1)%R. rewrite ltr_norml re1 andbT -(addr0 (-1)) ler_ltD //. by move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. pose e' : R := Num.min (r - fine (expand (contract r%:E - e%:num)))%R (fine (expand (contract r%:E + e%:num)) - r)%R. have e'0 : (0 < e')%R. rewrite /e' lt_minr; apply/andP; split. rewrite subr_gt0 -lte_fin -[in ltRHS](contractK r%:E). rewrite fine_expand // lt_expand// ?inE ?contract_le1 ?ltW//. by rewrite ltrBlDl ltrDr. rewrite subr_gt0 -lte_fin -[in ltLHS](contractK r%:E). by rewrite fine_expand// lt_expand ?inE ?contract_le1 ?ltrDl ?ltW. 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 // -ltrBlDl addrAC subrr add0r ltrNl. rewrite opprK -lte_fin fine_expand // => r'e'r _. exact: expand_ereal_ball_fin_lt. 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]. have {}re1 : contract r%:E = (1 - e%:num)%R. by move: re1; rewrite eq_sym -subr_eq => /eqP <-. have e1 : (1 < e%:num)%R. move: reN1. rewrite re1 -addrA -opprD ltrBlDl ltrBrDl -!mulr2n. rewrite -(mulr_natl e%:num) -{1}(mulr1 2%:R) => ?. by rewrite -(@ltr_pM2l _ 2). have Aoo : (setT `\ +oo `<=` A). 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). rewrite re1 opprB addrCA -[ltRHS]addr0 ltrD2 subr_lt0. by case/ltr_normlP : (contract_lt1 r'). rewrite /ereal_ball. rewrite re1 addrAC ltrBlDl ltrD // (lt_trans _ e1) // ltrNl. by move: (contract_lt1 r'); rewrite ltr_norml => /andP[]. rewrite /ereal_ball. rewrite [contract -oo]/= opprK gtr0_norm ?subr_gt0; last first. rewrite -ltrBlDl add0r ltrNl. by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. by rewrite re1 addrAC ltrBlDl ltrD. 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. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal