proposition: Lemma fsdist_conv_bind_left_distr (B : choiceType) p a b (f : A -> {dist B}) : (a <| p |> b) >>= f = (a >>= f) <| p |> (b >>= f).
proof: Proof. apply/fsdist_ext => b0 /=; rewrite fsdistbindE fsdist_convE. have [->|p0] := eqVneq p 0%:pr. by rewrite 2!conv0 fsdistbindE. have [->|p1] := eqVneq p 1%:pr. by rewrite 2!conv1 fsdistbindE. under eq_bigr do rewrite fsdist_convE avgR_mulDl avgRE. rewrite big_split -2!big_distrr /=. by rewrite -!fsdistbindEwiden // ?finsupp_conv_subl ?finsupp_conv_subr. 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