proposition: Lemma okup_apply_rule : forall (A B:Type)(a:Distr A)(f:A->Distr B)(r:U)(p:A->U)(q:B->U), okup r a p -> upfun p f (fun x => q) -> okup r (Mlet a f) q.
proof: Proof. unfold okup,upfun,Mlet; simpl; intros. apply Ole_trans with (mu a p); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)