proposition: Lemma fsdistbindA (A B C : choiceType) (m : {dist A}) (f : A -> {dist B}) (g : B -> {dist C}) : (m >>= f) >>= g = m >>= (fun x => f x >>= g).
proof: Proof. apply/val_inj/val_inj => /=; congr fmap_of_fsfun; apply/fsfunP => c. rewrite !fsdistbindE. under eq_bigr do rewrite fsdistbindE big_distrl. under [in RHS]eq_bigr do (rewrite fsdistbindE big_distrr /=; under eq_bigr do rewrite mulRA). rewrite exchange_big /= !big_seq; apply: eq_bigr => a a_m. rewrite supp_fsdistbind; apply/esym/big_fset_incl => [| b]. apply/fsubsetP => ? ?; apply/bigfcupP => /=. by exists (f a) => //; rewrite andbT in_imfset. case/bigfcupP => ?; rewrite andbT; case/imfsetP => ? /= ? -> ?. rewrite mem_finsupp negbK => /eqP ->. by rewrite mulR0 mul0R. 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