proposition: Lemma mufix_mu_le : forall x, mufix muF x <= mu (Mfix F x) (q x).
proof: Proof. intros; unfold mufix,Mfix; simpl. apply lub_le_compat; intros. intro n; generalize x; induction n; simpl; intros; auto. apply Ole_trans with (muF (fun y => mu (Miter F n y) (q y)) x0). apply (fmonotonic muF); auto. apply muF_F_le. intro y; unfold Mfix,fixp; simpl; intros f. apply le_lub with (c:=U) (f:=(Mu B @ (Ccpo.iter (D:=A -O-> cDistr B) F <o> y)) <_> f) (n:=n). Qed.
imports: ALEA(Probas) ALEA(Utheory)