proposition: Lemma pow_nmem (A B : {fset T}) : A \notin (powerset B) -> exists x, (x \in A) /\ (x \notin B).
proof: Proof. rewrite powersetE => P. apply (satr_notSub A B P). Qed.
imports: mathcomp(ssreflect ssrbool eqtype seq choice) CompDecModal.libs(edone bcase base fset)