proposition: Lemma close_trans (y x z : U) : close x y -> close y z -> close x z.
proof: Proof. rewrite !entourage_close => cxy cyz A entA. exact: entourage_split (cxy _ _) (cyz _ _). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed