proposition: Lemma summable_abs (S : T -> R) : summable \`|S| <-> summable S.
proof: Proof. have h J: \sum_(j <- J) `| `|S j| | = \sum_(j <- J) `|S j|. by apply/eq_bigr=> j _; rewrite normr_id. split=> /summable_seqP[M ge0_M leM]; apply/summable_seqP; by exists M=> // => J /leM; rewrite h. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology