proposition: Lemma fsumD X Y : fsum (X `\` Y) = fsum X - fsum (X `&` Y).
proof: Proof. rewrite fsumS (_ : [fset x in X | _] = X `&` Y) //. apply: fset_ext => x. by rewrite !inE negbK. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)