proposition: Lemma summableD (S1 S2 : T -> R) : summable S1 -> summable S2 -> summable (S1 \+ S2).
proof: Proof. case=> [M1 h1] [M2 h2]; exists (M1 + M2) => J /=. pose M := \sum_(x : J) (`|S1 (val x)| + `|S2 (val x)|). rewrite (@le_trans _ _ M) // ?ler_sum // => [K _|]. by rewrite ler_normD. by rewrite /M big_split lerD ?(h1, h2). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology