proposition: Lemma nbhs_fin_out_above r (e : {posnum R}) (A : set (\bar R)) : ereal_ball r%:E e%:num `<=` A -> (- 1 < contract r%:E - e%:num)%R -> (1 <= contract r%:E + e%:num)%R -> nbhs r%:E A.
proof: Proof. move=> reA reN1 re1. have er1 : (`|contract r%:E - e%:num| < 1)%R. rewrite ltr_norml reN1 andTb ltrBlDl ltr_pwDl //. by move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. pose e' := (r - fine (expand (contract r%:E - e%:num)))%R. 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 ltrBlDl ltrDr. 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.
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