proposition: Lemma separated_disjoint A B : separated A B -> A `&` B = set0.
proof: Proof. move=> AB; rewrite predeqE => x; split => // -[Ax Bx]. by move: AB; rewrite /separated => -[<- _]; split => //; apply: subset_closure. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed