proposition: Lemma fsdist1_inj (C : choiceType) : injective (@fsdist1 C).
proof: Proof. move=> a b /eqP ab; apply/eqP; apply: contraTT ab => ab. apply/eqP => /(congr1 (fun x : FSDist.t _ => x a)). rewrite !fsdist1E !inE eqxx (negbTE ab); exact: R1_neq_R0. 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