proposition: Lemma DsuppE : D = finsupp f.
proof: Proof. apply fsetP => a. rewrite /f /D !mem_finsupp !fsfunE; case: ifPn; last by rewrite eqxx. by case/imfsetP => b /= Hb ->; rewrite H // -mem_finsupp. 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