proposition: Lemma nbhs_oo_up_e1 (A : set (\bar R)) (e : {posnum R}) : (e%:num <= 1)%R -> ereal_ball +oo e%:num `<=` A -> nbhs +oo A.
proof: Proof. move=> e1 ooeA. exists (fine (expand (1 - e%:num)%R)); rewrite num_real; split => //. case => [r | | //]. - rewrite fine_expand; last first. by rewrite ger0_norm ?ltrBlDl ?ltrDr // subr_ge0. by move=> ?; exact/ooeA/expand_ereal_ball_pinfty. - by move=> _; exact/ooeA/ereal_ball_center. 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