proposition: Lemma within_nbhsW (x : T) : A x -> within A (nbhs x) `=>` globally A.
proof: Proof. move=> Ax P AP; rewrite /within/=; near=> y; apply: AP. 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