proposition: Lemma nbhs_fin_out_below r (e : {posnum R}) (A : set (\bar R)) : ereal_ball r%:E e%:num `<=` A -> (contract r%:E - e%:num <= - 1)%R -> (contract r%:E + e%:num < 1)%R -> nbhs r%:E A.
proof: Proof. move=> reA reN1 re1. have ? : (`|contract r%:E + e%:num| < 1)%R. rewrite ltr_norml re1 andbT (@lt_le_trans _ _ (contract r%:E)) // ?lerDl //. by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. 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 ?ltrDl ?ltW. 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.
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