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