proposition: Lemma Iincl_fix_ifix : forall x, Iincl (Imu (Mfix F x) (Q x)) (fixp (D:=A-O->IUcpo) ImuF x).
proof: Proof. assert (forall n x, Iincl (Imu (Miter F n x) (Q x)) (Ccpo.iter (D:=A-O->IUcpo) ImuF n x)). induction n; simpl; intros; auto. apply Iincl_trans with (ImuF (fun y => Imu (Miter F n y) (Q y)) x). apply Iincl_F_ImuF. intro y; unfold Mfix, fixp. intro f; simpl. apply le_lub with (f:=(Mu B @ (Ccpo.iter (D:=A -O-> cDistr B) F <o> y)) <_> f) (n:=n); auto. apply (fmonotonic ImuF); auto. intros; unfold Iincl, Imu,Mfix,fixp; simpl; split. apply lub_le_compat; intros. intro n; case (H n x); intros. apply Ole_trans with (low (Imu (Miter F n x) (Q x))); auto. apply lub_glb_le; intros; auto. case (H n x); intros. apply Ole_trans with (up (Imu (Miter F n x) (Q x))); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)