proposition: Lemma summableN (S : T -> R) : summable S -> summable (- S).
proof: Proof. case=> [M h]; exists M => J; rewrite (le_trans _ (h J)) //. rewrite le_eqVlt; apply/orP; left; apply/eqP/eq_bigr. by move=> /= K _; rewrite normrN. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology