proposition: Lemma fixrule_up_lub : forall (p : A -> natO -m> U), (forall (i:nat) (f:A->Distr B), (upfun (fun x => p x i) f q) -> upfun (fun x => p x (S i)) (fun x => F f x) q) -> upfun (fun x => lub (p x)) (Mfix F) q.
proof: Proof. red; red; intros. rewrite <- Ulub_lub. apply (fixrule_up_Ulub p H x). Qed.
imports: ALEA(Probas) ALEA(Utheory)