proposition: Lemma Mchoice_mon : forall (A:Type) (p:U) (m1 m2 n1 n2: Distr A), m1<=m2 -> n1<=n2 -> Mchoice p m1 n1 <= Mchoice p m2 n2.
proof: Proof. simpl; intros. apply Uplus_le_compat; repeat Usimpl; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)