proposition: Lemma fsum_eq0 X : fsum X = 0 -> {in X, const 0 w}.
proof: Proof. case: X => r i. suff {i} : \sum_(x <- r) w x = 0 -> {in r, const 0 w} by apply. move/eqP. elim: r => [_|y r IHr] //=. rewrite big_cons addn_eq0 => /andP [/eqP H /IHr H']. move => x. rewrite inE. case/orP => [/eqP ->|] //. exact: H'. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)