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