proposition: Lemma nbhs_oo_down_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 reA; suff h : nbhs +oo (-%E @` A). rewrite (_ : -oo = - +oo) // nbhsNe; exists (-%E @` A) => //. rewrite predeqE => x; split=> [[y [z Az <- <-]]|Ax]; rewrite ?oppeK //. by exists (- x); [exists x | rewrite oppeK]. apply (@nbhs_oo_up_e1 _ e) => // x x1e; exists (- x); last by rewrite oppeK. by apply/reA/ereal_ballN; rewrite oppeK. 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