proposition: Lemma sum_finseq S (r : seq T) : uniq r -> {subset [pred x | S x != 0] <= r} -> sum S = \sum_(x <- r) S x.
proof: Proof. move=> eqr domS; rewrite /sum !(psum_finseq eqr). + move=> x; rewrite !inE => xPS; apply/domS; rewrite !inE. move: xPS; rewrite /fpos normr_eq0. by apply: contra => /eqP ->; rewrite maxxx. + move=> x; rewrite !inE => xPS; apply/domS; rewrite !inE. move: xPS; rewrite /fneg normr_eq0. by apply: contra => /eqP ->; rewrite minxx. rewrite -sumrB; apply/eq_bigr=> i _. by rewrite !ger0_norm ?(ge0_fpos, ge0_fneg) ?fposBfneg. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology