proposition: Lemma properSub (A B : {fset T}): A `<` B = (A `<=` B) && ~~ (B `<=` A).
proof: Proof. rewrite properEneq eqEsub. by case (A`<=`B), (B`<=`A). Qed.
imports: mathcomp(ssreflect ssrbool eqtype seq choice) CompDecModal.libs(edone bcase base fset)