proposition: Lemma cut_sub (A B : {fset T}) : A `<=` B \/ ~~ (A `<=` B).
proof: Proof. case (A `<=` B); first by left. right. by apply negbT. Qed.
imports: mathcomp(ssreflect ssrbool eqtype seq choice) CompDecModal.libs(edone bcase base fset)