proposition: Lemma ssum_seq_finsuppE (d : {dist C}) : \ssum_i scalept (fdist_of_fs d i) (S1 (fsval i)) = \ssum_(i <- finsupp d) scalept (d i) (S1 i).
proof: Proof. under eq_bigr do rewrite fdist_of_fsE. by rewrite ssum_seq_finsuppE'. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(finmap) Reals mathcomp(mathcomp_extra) mathcomp(classical_sets boolp cardinality Rstruct reals) mathcomp(ereal topology esum measure probability) ssrR realType_ext Reals_ext ssr_ext ssralg_ext bigop_ext fdist convex