proposition: Lemma nbhs_oo_down_1e (A : set (\bar R)) (e : {posnum R}) : (1 < e%:num)%R -> ereal_ball -oo e%:num `<=` A -> nbhs -oo A.
proof: Proof. move=> e1 reA; have [e2{e1}|e2] := ltrP 2 e%:num. suff -> : A = setT by exists 0%R. 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 /= lerBlDl. 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. apply/reA/ereal_ballN; rewrite /= oppeK. by apply: le_ereal_ball ye => /=; rewrite lerBlDl lerDr. 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