proposition: Lemma le1 (d : t) a : d a <= 1.
proof: Proof. have [ad|?] := boolP (a \in finsupp d); last by rewrite fsfun_dflt. rewrite -(f1 d) (big_fsetD1 _ ad)/=; apply/leR_addl. by apply/RleP/sumr_ge0 => ? _; exact/RleP/ge0. 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