proposition: Lemma d0 (x : T) : 0 <= d x.
proof: Proof. case/boolP: (x \in finsupp d); first by move/d0'/ltW. by move/fsfun_dflt ->; exact: lexx. 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 mathcomp(measure probability)