proposition: Lemma mufix_mu : (forall f x, f <= Mfix F -> mu (F f x) (q x) == muF (fun y => mu (f y) (q y)) x) -> forall x, mufix muF x == mu (Mfix F x) (q x).
proof: Proof. intros; apply Ole_antisym; auto. apply mufix_mu_le; intros; auto. rewrite (H f x0); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)