proposition: Lemma satr_nmemSup (a:T) (A B : {fset T}) : a \notin A -> B `<=` A -> a \notin B.
proof: Proof. move => P Q. case R: (a \in B) => //. by rewrite (subP Q) in P. Qed.
imports: mathcomp(ssreflect ssrbool eqtype seq choice) CompDecModal.libs(edone bcase base fset)