proposition: Lemma setCI2_r A B C : A -s (B \cap C) = (A -s B) \cup (A -s C).
proof: Proof. set_extens t. case/setC_P => ta tbc; apply/setU2_P; case:(setI2_ni tbc)=> tb; fprops. by case/setU2_P; case/setC_P => ta tc; apply/setC_P; split => //; case /setI2_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)