proposition: Lemma near_bind (T : topologicalType) (P Q : set T) (x : T) : (\near x, (\near x, P x) -> Q x) -> (\near x, P x) -> \near x, Q x.
proof: Proof. move=> PQ xP; near=> y; apply: (near PQ y) => //; by apply: (near (near_join xP) y). 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