proposition: Lemma summablebN (S : T -> R) : `[< summable (- S)>] = `[< summable S >].
proof: Proof. apply/asboolP/asboolP => /summableN //. by apply/eq_summable => x /=; rewrite opprK. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology