proposition: Lemma Ifixrule : (forall x:A, Iin 0 (I x O)) -> (forall (i:nat) (f:A->Distr B), (Iokfun (fun x => I x i) f Q) -> Iokfun (fun x => I x (S i)) (fun x => F f x) Q) -> Iokfun (fun x => Ilim (I x)) (Mfix F) Q.
proof: Proof. red; intros p0 Hrec. assert (forall n:nat, (Iokfun (fun x => (I x n)) (fun x => Miter F n x) Q)). induction n; simpl; auto. split. rewrite low_lim; rewrite low_Imu. apply lub_le; auto. intro n; apply Ole_trans with (low (Imu (Miter F n x) (Q x))). case (H n x); auto. rewrite low_Imu; apply Mfix_le_iter; auto. rewrite up_lim; rewrite up_Imu. unfold Mfix,mu_lub; simpl. apply lub_glb_le; intros. case (H n x); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)