proposition: Lemma Mfix_continuous : forall (Fn : natO -m> (A -O-> cDistr B) -M-> A -O-> cDistr B), (forall n, continuous (Fn n)) -> Mfix (lub Fn) <= lub (MFix A B @ Fn).
proof: Proof. unfold Mfix, MFix; intros; apply fixp_continuous; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)