proposition: Lemma okup_le_compat : forall (A:Type) (p p':U) (e:Distr A) (q q':A-o>U), p <= p' -> q' <= q -> okup p e q -> okup p' e q'.
proof: Proof. unfold okup; intros. apply Ole_trans with p; auto. apply Ole_trans with (mu e q); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)