proposition: Lemma mu_fplusok : forall (A : Type)(m:distr A) f g, fplusok f g -> mu m f <= [1-] mu m g.
proof: Proof. intros; apply Ole_trans with (mu m (finv g)); auto. apply (mu_stable_inv m g). Qed.
imports: ALEA(Monads) ALEA(Utheory)