proposition: Lemma setCU2_l A B C : (A \cup B) -s C = (A -s C) \cup (B -s C).
proof: Proof. set_extens t. case/setC_P => /setU2_P [] tab tc; apply/setU2_P; fprops. case/setU2_P => /setC_P [tab tc];apply/setC_P; split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)