proposition: Lemma fdist_conv_bind_left_distr (R : realType) (A B : finType) p a b (f : A -> fdist R B) : (a <| p |> b) >>= f = (a >>= f) <| p |> (b >>= f).
proof: Proof. apply/fdist_ext => a0 /=; rewrite !(fdistbindE,fdist_convE) /=. rewrite 2!big_distrr /= -big_split /=; apply/eq_bigr => a1 _. by rewrite fdist_convE mulrDl !mulrA. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext