proposition: Lemma setC_ni x A B: ~inc x (A -s B) -> (~ inc x A \/ inc x B).
proof: Proof. move => h; case: (inc_or_not x B) => nxb; [by right | left]. move => xa; case: h; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)