proposition: Lemma closeEnbhs x : close x = cluster (nbhs x).
proof: Proof. transitivity (cluster (open_nbhs x)); last first. by rewrite /cluster; under eq_fun do rewrite -meets_openl. rewrite clusterEonbhs /close funeqE => y /=; rewrite meetsC /meets. apply/eq_forall => A; rewrite forall_swap. by rewrite closureEonbhs/= meets_globallyl. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed