proposition: Lemma sum_nat_eq0 (I : finType) (P : pred I) (E : I -> nat) : (\sum_(i | P i) E i == 0)%N = [forall (i | P i), E i == 0%N].
proof: Proof. by rewrite eq_sym -(@leqif_sum I P _ (fun _ => 0%N) E) ?big1_eq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)