proposition: Lemma ge0 (d : t) a : 0 <= d a.
proof: Proof. case: d => /= [f /andP[/allP f0 _]]. have [/f0/RltP/ltRW|/fsfun_dflt->] := boolP (a \in finsupp f); first exact. by apply/RleP; rewrite 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