proposition: Lemma sum_nat_seq_eq0 (I : eqType) r (P : pred I) (E : I -> nat) : (\sum_(i <- r | P i) E i == 0) = all [pred i | P i ==> (E i == 0)] r.
proof: Proof. rewrite big_tnth sum_nat_eq0; apply/forallP/allP => /= HE x. by move=> /seq_tnthP[i ->]; apply: HE. by apply: HE; rewrite mem_tnth. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap