proposition: Lemma set_CI2 A B X: X -s (A\cap B) = (X -s A) \cup (X -s B).
proof: Proof. set_extens t. case/setC_P => tX tu; apply/setU2_P; case: (setI2_ni tu) => ti; fprops. by case /setU2_P => /setC_P [ta tab]; apply/setC_P;split => //; case/setI2_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)