proposition: Lemma le_summable (F1 F2 : T -> R) : (forall x, 0 <= F1 x <= F2 x) -> summable F2 -> summable F1.
proof: Proof. move=> le_F [M leM]; exists M => J; apply/(le_trans _ (leM J)). apply/ler_sum => /= j _; case/andP: (le_F (val j)) => h1 h2. by rewrite !ger0_norm // (le_trans h1 h2). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology