proposition: Lemma fixrule_up_Ulub : forall (p : A -> natO -> 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 => Ulub (p x)) (Mfix F) q.
proof: Proof. red; red; intros. unfold Mfix; simpl. apply Ole_trans with (Ulub ((Mu B @ (Miter F <o> x)) <_> q x)); auto. apply Ulub_le_compat. intro n; generalize x; induction n; simpl; intros; auto. apply (H n (Miter F n) IHn x0). Qed.
imports: ALEA(Probas) ALEA(Utheory)