proposition: Lemma eq0_psum (f : T -> R) : summable f -> psum f = 0 -> (forall x : T, f x = 0).
proof: Proof. move=> sm psum_eq0 x; apply/eqP; rewrite -normr_eq0. rewrite eq_le normr_ge0 andbT -psum_eq0. apply/(le_trans _ (gerfinseq_psum (r := [:: x]) _ sm)) => //. by rewrite big_seq1. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology