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