proposition: Lemma eq_summableb (S1 S2 : T -> R) : (S1 =1 S2) -> `[< summable S2 >] = `[< summable S1 >].
proof: Proof. by move=> eq_12; apply/asboolP/asboolP; apply/eq_summable. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology