proposition: Lemma setC_ne A B: ssub A B -> nonempty (B -s A).
proof: Proof. move=> [s neq]; apply /nonemptyP;dneg ceq; move: (empty_setC ceq). by apply: extensionality. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)