proposition: Lemma ok_inv : forall (A:Type)(p:U)(e:Distr A)(f : A -> U), ok p e f -> mu e (finv f) <= [1-]p.
proof: Proof. unfold ok; intros A p e f oka. apply Ole_trans with ([1-](mu e f)); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)