proposition: Lemma BindE (A B : choiceType) m (f : A -> [the monad of acto] B) : (m >>= f) = (m >>= f)%fsdist.
proof: Proof. by rewrite /hierarchy.bind /= /bind. Qed.
imports: Reals mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals Rstruct) infotheo(Reals_ext realType_ext ssr_ext fsdist) infotheo(convex) HB(structures) monae_lib hierarchy monad_lib proba_lib