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