proposition: Lemma psumN (S : T -> R) : psum (- S) = psum S.
proof: Proof. case/boolP: `[< summable S >] => h; last first. by rewrite !psum_out ?oppr0 //; apply/asboolPn; rewrite ?summablebN. rewrite /psum summablebN h; apply/eq_ppsum=> J /=. by apply/eq_bigr=> j _; rewrite normrN. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology