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