proposition: Lemma summable_funepos D f : summable D f -> summable D f^\+.
proof: Proof. apply: le_lt_trans; apply le_esum => t Dt. by rewrite -/((abse \o f) t) fune_abse gee0_abs// leeDl. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology sequences normedtype numfun