proposition: Lemma fsdist1map (C : choiceType) (d : {dist C}) (c : C) : fsdistmap (@fsdist1 C) d (fsdist1 c) = d c.
proof: Proof. rewrite fsdistmapE. case/boolP: (c \in finsupp d)=> ifd. by rewrite fbig_pred1_inj //; apply: fsdist1_inj. transitivity(\sum_(a <- finsupp d | a == c) d a). by apply eq_bigl=> j; apply/eqtype.inj_eq/fsdist1_inj. rewrite big_seq_cond big_pred0; last first. by move=> j; apply/andP; case=> jfd /eqP ji; move: jfd; rewrite ji (negbTE ifd). by rewrite fsfun_dflt. 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