proposition: Lemma nbhs_nbhs (p : M) A : nbhs p A -> nbhs p (nbhs^~ A).
proof: Proof. rewrite nbhsE nbhs_E => - [B entB sBpA]. have /entourage_split_ex[C entC sC2B] := entB. exists C => // q Cpq; rewrite nbhs_E; exists C => // r Cqr. by apply/sBpA/sC2B; exists q. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed