proposition: Lemma clopen_separatedP A : clopen A <-> separated A (~` A).
proof: Proof. split=> [[oA cA]|[] /[!(@disjoints_subset T)] /[!(@setCK T)] clAA AclA]. rewrite /separated -((closure_id A).1 cA) setICr ; split => //. by rewrite -((closure_id _).1 (open_closedC oA)) setICr. split; last by rewrite closure_id eqEsubset; split => //; exact: subset_closure. by rewrite -closedC closure_id eqEsubset; split; [exact: subset_closure|exact: subsetCr]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed