proposition: Lemma upfun_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 -> upfun p e q -> upfun p' e q'.
proof: Proof. unfold upfun; intros. apply okup_le_compat with (p x) (q x); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)