proposition: Lemma psum_eq0 (f : T -> R) : (forall x, f x = 0) -> psum f = 0.
proof: Proof. by move=> eq; rewrite (eq_psum eq) psum0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology