proposition: Lemma summablebDl (S1 S2 : T -> R) : summable S1 -> `[< summable (S1 \+ S2) >] = `[< summable S2 >].
proof: Proof. move=> sm1; apply/asboolP/asboolP; last by apply/(summableD sm1). move=> sm12; apply/(@eq_summable _ _ ((S1 \+ S2) \- S1)). by move=> x /=; rewrite addrC addKr. by apply/summableD/summableN. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology