proposition: Lemma nbhs_fin_out_above_below r (e : {posnum R}) (A : set (\bar R)) : ereal_ball r%:E e%:num `<=` A -> (contract r%:E - e%:num < -1)%R -> (1 < contract r%:E + e%:num)%R -> nbhs r%:E A.
proof: Proof. move=> reA reN1 re1; suff : A = setT by move->; apply: filterT. rewrite predeqE => x; split => // _; apply reA. case: x => [r'| |] //. - have [?|?] := lerP r r'. + by apply: contract_ereal_ball_fin_le => //; exact/ltW. + by apply contract_ereal_ball_fin_lt => //; exact/ltW. - exact/contract_ereal_ball_pinfty. - apply/ereal_ballN/contract_ereal_ball_pinfty. by rewrite EFinN contractN -(opprK 1%R) ltrNl opprD opprK. 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