proposition: Lemma sumID S (P : pred T) : summable S -> sum S = sum (fun x => (P x)%:R * S x) + sum (fun x => (~~ P x)%:R * S x).
proof: Proof. move=> sm_S; rewrite /sum addrACA -[in RHS]opprD; congr (_ - _). + rewrite (psumID P); first by apply/summable_fpos. by congr (_ + _); apply/eq_psum => x; rewrite fpos_natrM. + rewrite (psumID P); first by apply/summable_fneg. by congr (_ + _); apply/eq_psum => x; rewrite fneg_natrM. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology