proposition: Lemma cut_mem a (A: {fset T}) : a \in A \/ a \notin A.
proof: Proof. case (a \in A); first by left. right. by apply negbT. Qed.
imports: mathcomp(ssreflect ssrbool eqtype seq choice) CompDecModal.libs(edone bcase base fset)