proposition: Lemma eq_psum (F1 F2 : T -> R) : F1 =1 F2 -> psum F1 = psum F2.
proof: Proof. move=> eq_12; rewrite /psum (eq_summableb eq_12). case: `[< summable F1 >] => //. congr sup. rewrite predeqE => x; split=> -[J ->]; exists J; by apply/eq_bigr=> /= K _; rewrite eq_12. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology