proposition: Lemma right_neutral : BindLaws.right_neutral bind ret.
proof: Proof. by move=> ? ?; exact: fsdistbind1. 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