proposition: Lemma satr_notSub (A B : {fset T}) : ~~ (A `<=` B) -> exists a, (a \in A) /\ (a \notin B).
proof: Proof. move => P. move: (subPn A B P) => {P} [a P Q]. by exists a. Qed.
imports: mathcomp(ssreflect ssrbool eqtype seq choice) CompDecModal.libs(edone bcase base fset)