proposition: Lemma Iok_le_compat : forall (A:Type) (I J:IU) (e:Distr A) (F G:A->IU), Iincl I J -> (forall x, Iincl (G x) (F x)) -> Iok I e F -> Iok J e G.
proof: Proof. unfold Iok; intros; apply Iincl_trans with I; auto. apply Iincl_trans with (Imu e F); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)