proposition: Lemma fdistbindA R A B C (m : fdist R A) (f : A -> fdist R B) (g : B -> fdist R C) : (m >>= f) >>= g = m >>= (fun x => f x >>= g).
proof: Proof. apply/fdist_ext => c; rewrite !fdistbindE /=. rewrite (eq_bigr (fun a => \sum_(a0 in A) m a0 * f a0 a * g a c)%R); last first. by move=> b _; rewrite fdistbindE big_distrl. rewrite exchange_big /=; apply eq_bigr => a _. by rewrite fdistbindE big_distrr /=; apply eq_bigr => b _; rewrite 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