proposition: Lemma okup_ifrule : forall (A:Type)(b:(Distr bool))(f1 f2:Distr A)(p1 p2:U)(q:A->U), okup p1 f1 q -> okup p2 f2 q -> okup (p1 * (mu b ctrue) + p2 * (mu b cfalse)) (Mif b f1 f2) q.
proof: Proof. unfold okup; intros. rewrite (Mif_eq b f1 f2 q). apply Uplus_le_compat. apply Umult_le_compat_left; auto. apply Umult_le_compat_left; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)