proposition: Lemma nbhs_interval (R : realFieldType) (P : R -> Prop) (r : R) (a b : \bar R) : a < r%:E -> r%:E < b -> (forall y, a < y%:E -> y%:E < b -> P y) -> nbhs r P.
proof: Proof. move => ar rb abP; case: (lt_ereal_nbhs ar rb) => d rd. exists d%:num => //= y; rewrite /= distrC. by move=> /rd /andP[? ?]; apply: abP. 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