proposition: Lemma setCId_Pl A B: A -s B = A <-> disjoint A B.
proof: Proof. split => eq1. apply/(disjoint_subsets_P (@sub_refl A)); rewrite eq1; fprops. apply:extensionality; first by apply:sub_setC. move => t tA; apply/setC_P;split => // tB; empty_tac1 t. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)