proposition: Lemma mu_le_plus : forall (A : Type)(m:distr A) (f g:MF A), mu m (fplus f g) <= mu m f + mu m g.
proof: Proof. intros; apply Ole_trans with (mu m (fplus (fminus f (fesp f g)) g)). apply mu_monotonic. unfold fplus,fminus,fesp; intros; auto. rewrite (mu_stable_plus m (f:=fminus f (fesp f g)) (g:=g)). Usimpl; auto. red; unfold fminus,fesp,finv; intro x; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)