proposition: Lemma psum_sup_seq S : psum S = sup [set x | exists2 J : seq T, uniq J & x = \sum_(x <- J) `|S x| ]%classic.
proof: Proof. rewrite psum_sup; congr sup; rewrite predeqE => x; split. case=> J ->; exists (enum_fset J). by case: J => /= J /canonical_uniq. by rewrite (big_fset_seq \`|_|) /=. case=> J uqJ ->; exists [fset x in J]. by rewrite (big_seq_fset \`|_|). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology