proposition: Lemma mu_esp_zero : forall (A:Type)(m:distr A)(f g:MF A), mu m (finv f) <= 0 -> mu m g == mu m (fesp f g).
proof: Proof. intros; apply Ole_antisym. apply Ole_trans with (([1-](mu m (finv f))) & mu m g); auto. apply Ole_trans with (1 & mu m g); auto. apply Uesp_le_compat; auto. apply Ole_trans with ([1-]0); auto. apply mu_monotonic; unfold fesp; intro x; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)