proposition: Lemma eq_psum_abs (S1 S2 : T -> R) : \`|S1| =1 \`|S2| -> psum S1 = psum S2.
proof: Proof. by move=> eqS; rewrite -[LHS]psum_abs -[RHS]psum_abs; apply/eq_psum. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology