proposition: Lemma fixrule_Ulub : forall (p : A -> natO -> U), (forall x:A, p x O == 0)-> (forall (i:nat) (f:A->Distr B), (okfun (fun x => p x i) f q) -> okfun (fun x => p x (S i)) (fun x => F f x) q) -> okfun (fun x => Ulub (p x)) (Mfix F) q.
proof: Proof. red; intros p p0 Hrec. assert (forall n:nat, (okfun (fun x => (p x n)) (fun x => Miter F n x) q)). induction n; simpl; auto. red; red; intros; auto. red; intros. apply Ulub_le; auto. intro n; apply Ole_trans with (mu (Miter F n x) (q x)). apply (H n). apply Mfix_le_iter; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)