proposition: Lemma fdist_Rgt0 (A : finType) (d : real_realType.-fdist A) a : (d a != 0) <-> (0 < d a)%coqR.
proof: Proof. by rewrite fdist_gt0; split=> /RltP. 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