proposition: Lemma mu_stable_inv_inv : forall (A:Type) (m:distr A)(f : MF A), mu m f <= [1-] mu m (finv f).
proof: Proof. intros; apply Ole_trans with (mu m (finv (finv f))). apply (mu_monotonic m); auto. intro x; unfold finv; auto. apply (mu_stable_inv m); auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)