proposition: Lemma fsdistbindEwiden S x : finsupp p `<=` S -> fsdistbind x = \sum_(a <- S) p a * (g a) x.
proof: Proof. move=> suppS; rewrite fsdistbindE (big_fset_incl _ suppS) //. by move=> a2 Ha2; rewrite memNfinsupp => /eqP ->; rewrite mul0R. 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