proposition: Lemma psum_finseq S (r : seq.seq T) : uniq r -> {subset [pred x | S x != 0] <= r} -> psum S = \sum_(x <- r) `|S x|.
proof: Proof. move=> eq_r ler; set s := RHS; have h J: uniq J -> \sum_(x <- J) `|S x| <= s. move=> uqJ; rewrite (bigID (ssrbool.mem r)) /= addrC big1. move=> x xNr; apply/eqP; apply/contraR: xNr. by rewrite normr_eq0 => /ler. rewrite add0r {}/s -big_filter; set s := seq.filter _ _. rewrite [X in _<=X](bigID (ssrbool.mem J)) /=. rewrite (perm_big [seq x <- r | x \in J]) /=. apply/uniq_perm; rewrite ?filter_uniq // => x. by rewrite !mem_filter andbC. by rewrite big_filter lerDl sumr_ge0. case/summable_of_bd: h => smS le_psum; apply/eqP. by rewrite eq_le le_psum /=; apply/gerfinseq_psum. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology