proposition: Lemma f0 a : a \in finsupp f -> 0 < f a.
proof: Proof. rewrite mem_finsupp /f fsfunE; case: ifPn => Ha; last by rewrite eqxx. rewrite -mem_finsupp; exact/FSDist.gt0. 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