proposition: Lemma fsetDSS X X' Y Y' : X `<=` X' -> Y' `<=` Y -> X `\` Y `<=` X' `\` Y'.
proof: Proof. move=> HX /subP HY. apply: sep_sub => // x _. exact: contra (HY _). Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)