proposition: Lemma ssum_widen_finsupp (x : {dist C}) X : (finsupp x `<=` X)%fset -> \ssum_(i <- finsupp x) scalept (x i) (S1 i) = \ssum_(i <- X) scalept (x i) (S1 i).
proof: Proof. move=> xX. rewrite [in RHS](bigID (fun i => i \in finsupp x)) /=. have -> : (\ssum_(i <- X | i \notin finsupp x) scalept (x i) (S1 i)) = Zero by rewrite big1 //= => i Hi; rewrite fsfun_dflt // scale0pt. rewrite addpt0 [in RHS]big_fset_condE /=. suff H : finsupp x = [fset i | i in X & i \in finsupp x]%fset by rewrite [in LHS]H. apply/eqP; rewrite eqEfsubset; apply/andP; split; apply/fsubsetP=> c; rewrite !inE /=. - by move=> cfx; move/fsubsetP/(_ c):xX ->. - by case/andP. 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