proposition: Lemma fsdist10 a0 : a0 != a -> fsdist1 a0 = 0.
proof: Proof. by move=> a0a; rewrite fsdist1E /D inE (negbTE a0a). 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