proposition: Lemma eq_sum (F1 F2 : T -> R) : F1 =1 F2 -> sum F1 = sum F2.
proof: Proof. move=> eq_fg; rewrite /sum; congr (_ - _); apply/eq_psum. by apply/eq_fpos. by apply/eq_fneg. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology