proposition: Lemma fsdistmap_comp (A B C : choiceType) (g : B -> C) (h : A -> B) : fsdistmap (g \o h) = fsdistmap g \o fsdistmap h.
proof: Proof. rewrite boolp.funeqE => d; rewrite /fsdistmap /= fsdistbindA; congr (_ >>= _). by rewrite boolp.funeqE => a; rewrite fsdist1bind. 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