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