proposition: Lemma Mlet_continuous_right : forall a:Distr A, continuous (D1:=A-O->cDistr B) (D2:=cDistr B) (MLet A B a).
proof: Proof. red; intros; intro f. rewrite (MLet_simpl (A:=A) (B:=B)). apply Ole_trans with (mu a (fun x:A => lub ((Mu B @ (h <o> x)) <_> f))); auto. apply Ole_trans with (mu a (lub (c:=A-O->U) (ford_shift (fun x:A => ((Mu B @ (h <o> x)) <_> f))))); auto. apply Ole_trans with (1 := mu_continuous a (ford_shift (fun x : A => (Mu B @ (h <o> x)) <_> f))); auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)