proposition: Lemma fsumU X Y : fsum (X `|` Y) = fsum X + fsum Y - fsum (X `&` Y).
proof: Proof. apply/eqP. rewrite [fsum (_ `|` _)](fsumID (mem X)) /=. rewrite (_ : [fset x in X `|` Y | x \in X] = X); last by apply: fset_ext => x; rewrite !inE; bcase. rewrite (_ : [fset x in X `|` Y | x \notin X] = Y `\` X); last by apply: fset_ext => x; rewrite !inE; bcase. rewrite fsumD addnBA fsetIC //. by rewrite fsetIC fsumI leq_subr. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)