proposition: Lemma separatedC A B : separated A B = separated B A.
proof: Proof. by rewrite /separated andC setIC (setIC _ B). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed