proposition: Lemma mu_le_esp_inv : forall (A:Type) (m:distr A)(f g : MF A), ([1-]mu m (finv f)) & mu m g <= mu m (fesp f g).
proof: Proof. intros; rewrite Uesp_sym. apply Uplus_inv_le_esp; Usimpl. apply Ole_trans with (mu m (fplus (fesp f g) (finv f))); auto. apply (mu_monotonic m); unfold fplus, fesp,finv; simpl; intros. rewrite Uesp_sym; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)