proposition: Lemma le_psum_abs (S1 S2 : T -> R) : (forall x, `|S1 x| <= `|S2 x|) -> summable S2 -> psum S1 <= psum S2.
proof: Proof. move=> leS smS2; rewrite -[X in X<=_]psum_abs -[X in _<=X]psum_abs. by apply/le_psum/summable_abs => // x; rewrite normr_ge0 leS. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology