proposition: Lemma Mdiv_continuous : forall A (k:U)(d:distr A), continuous (Mdiv k (mu d)).
proof: Proof. red; intros; repeat rewrite Mdiv_simpl. apply Ole_trans with (lub (mu d @ h) / k); auto. exact (Udiv_continuous k (mu d @ h)). Qed.
imports: ALEA(Monads) ALEA(Utheory)