proposition: Lemma setI2_ni x A B: ~inc x (A\cap B) -> (~ inc x A \/ ~ inc x B).
proof: Proof. move => h; case: (inc_or_not x A); fprops => xa; right => xB; case: h; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)