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