proposition: Lemma Mif_mon : forall (A:Type) (b1 b2:Distr bool) (m1 m2 n1 n2: Distr A), b1 <= b2 -> m1 <= m2 -> n1 <= n2 -> Mif b1 m1 n1 <= Mif b2 m2 n2.
proof: Proof. intros; unfold Mif. apply Mlet_le_compat ; auto. intro x; destruct x; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)