proposition: Lemma entourage_sym {X Y : Type} E (x : X) (y : Y) : E (x, y) <-> (E ^-1)%classic (y, x).
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed