proposition: Lemma summable_fpos (f : T -> R) : summable f -> summable (fpos f).
proof: Proof. move/summable_abs; apply/le_summable=> x. by rewrite ge0_fpos /= le_fpos_norm. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology