proposition: Lemma f1 (d : t) : \sum_(a <- finsupp d) d a = 1.
proof: Proof. by case: d => f /= /andP[_ /eqP]. 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