proposition: Lemma ssum_seq_finsuppE' (d x : {dist C}) : \ssum_(i : fdist_of_FSDist.D d) scalept (x (fsval i)) (S1 (fsval i)) = \ssum_(i <- finsupp d) scalept (x i) (S1 i).
proof: Proof. by rewrite (ssum_seq_finsuppE'' idfun). 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