proposition: Lemma psum_abs (S : T -> R) : psum \`|S| = psum S.
proof: Proof. rewrite /psum; do 2! case: ifPn => //; first last. + by move/asboolP/summable_abs/asboolP=> ->. + by move/asboolPn/summable_abs/asboolPn=> /negbTE->. move=> _ _; congr sup; rewrite predeqE => x; split. case=> J ->; exists J. by under eq_bigr do rewrite normr_id. case=> J ->; exists J. by under [in RHS]eq_bigr do rewrite normr_id. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology