proposition: Lemma setIC2 A B C: A \cap (B -s C) = A \cap B -s (A \cap C).
proof: Proof. set_extens t. move => /setI2_P [tA /setC_P [tb ntc]]; apply /setC_P; split; fprops. by move /setI2_P => []. move => /setC_P [/setI2_P [ha hb] /setI2_P hc]; apply/setI2_P; split => //. by apply/setC_P; split => //; dneg hd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)