proposition: Lemma Mlet_le_compat : forall (A B : Type) (m1 m2:Distr A) (M1 M2 : A-o> Distr B), m1 <= m2 -> M1<=M2 -> Mlet m1 M1 <= Mlet m2 M2.
proof: Proof. unfold Mlet,star; simpl; intros A B m1 m2 M1 M2 Hm HM f. apply Ole_trans with (mu m2 (fun x : A => mu (M1 x) f)); auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)