proposition: Lemma Mfixvar_up : (forall (f:A->Distr B), upfun (fun x => Loop (fun y => mu (f y) (q y)) x) (fun x => F f x) q) -> upfun up_loop (Mfix F) q.
proof: Proof. intros; unfold up_loop,nufix; simpl. apply okup_fixrule_glb with (p:=fun x => (Ccpo.iter (G Loop)) <o> x); simpl; intros;intro; auto. unfold upfun,okup in *|-*. red; apply Ole_trans with (1:=H f x). rewrite Loop_eq. apply (mu_monotonic (stop x)); intro x0. case x0; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)