proposition: Lemma dnbhs_ball (a : M) (e : R) : (0 < e)%R -> a^' (ball a e `\ a).
proof: Proof. move: e => _/posnumP[e]; rewrite /dnbhs /within /=; near=> r => ra. split => //=; last exact/eqP. by near: r; rewrite near_simpl; exact: near_ball. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed