proposition: Lemma Iin_mu_Imu : forall (A:Type) (e:Distr A) (F:A->IU) (f:A->U), (forall x, Iin (f x) (F x)) -> Iin (mu e f) (Imu e F).
proof: Proof. unfold Iin,Imu; simpl; split. apply (mu_monotonic e); intro x; case (H x); auto. apply (mu_monotonic e); intro x; case (H x); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)