proposition: Lemma fsumID p X : fsum X = fsum [fset x in X | p x ] + fsum [fset x in X | ~~ p x].
proof: Proof. by rewrite /fsum (bigID p) /= !big_sep. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)