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