proposition: Lemma supp_fsdistmap (A B : choiceType) (f : A -> B) d : finsupp (fsdistmap f d) = [fset f x | x in finsupp d].
proof: Proof. rewrite /fsdistmap supp_fsdistbind; apply/fsetP => d'. apply/bigfcupP/imfsetP => [[D]|]. rewrite andbT => /imfsetP[a /=] ad ->{D}. by rewrite supp_fsdist1 inE => /eqP ->{d'}; exists a. case=> a /= ad -> {d'}; exists (fsdist1 (f a)). by rewrite andbT; apply/imfsetP; exists a. by rewrite supp_fsdist1 inE. 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