proposition: Lemma Mlet_lub_le : forall (mun:natO-m>cDistr A) (Mn : natO-m>(A-O->cDistr B)), Mlet (lub mun) (lub Mn) <= lub (c:=cDistr B) ((MLet A B @2 mun) Mn).
proof: Proof. intros; apply Mlet_continuous2 with (f:=mun) (g:=Mn). Qed.
imports: ALEA(Monads) ALEA(Utheory)