proposition: Lemma summable_fneg (f : T -> R) : summable f -> summable (fneg f).
proof: Proof. by move/summableN/summable_fpos/(eq_summable (fposN _)). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology