proposition: Lemma Imu_monotonic : forall (A:Type) (e:Distr A) (F G : A -> IU), (forall x, Iincl (F x) (G x)) -> Iincl (Imu e F) (Imu e G).
proof: Proof. unfold Iincl,Imu; simpl; intuition. 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)