proposition: Lemma fsdist_supp_neq0 (d : {dist A}) : finsupp d != fset0.
proof: Proof. apply/eqP => d0. by move: (FSDist.f1 d); rewrite d0 big_nil => /esym; exact: R1_neq_R0. 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