proposition: Lemma psum0 : psum (fun _ : T => 0) = 0 :> R.
proof: Proof. rewrite /psum asboolT; first by apply/summable0. set S := [set x | _]%classic; suff: S = (set1 0). by move => ->; rewrite sup1. rewrite predeqE => x; split. by case=> J -> /=; rewrite big1 // normr0. by move=> ->; exists fset0; rewrite big_fset0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology