proposition: Lemma fsumDsub X Y : Y `<=` X -> fsum (X `\` Y) = fsum X - fsum Y.
proof: Proof. move => /subP sub. rewrite fsumD [_ `&` _](_ : _ = Y) //. apply/eqP. rewrite eqEsub fsubIr /=. apply/subP => x Hx. by rewrite inE Hx (sub _ Hx). Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)