proposition: Lemma entourage_split_ent (A : set (M * M)) : entourage A -> entourage (split_ent A).
proof: Proof. by move=> /split_entP []. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed