proposition: Lemma neq0_psum (f : T -> R) : psum f <> 0 -> exists x : T, f x <> 0.
proof: Proof. by move=> nz_psum; apply/existsp_asboolPn/asboolPn => /psum_eq0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology