proposition: Lemma fsetUD X Y : Y `<=` X -> Y `|` (X `\` Y) = X.
proof: Proof. move/subP => sub. apply: fset_ext => x. rewrite !inE. case e: (x \in Y) => //=. by rewrite (sub _ e). Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)