proposition: Lemma mu_stable_le_minus : forall (A:Type) (m:distr A)(f g : MF A), mu m f - mu m g <= mu m (fun x => f x - g x).
proof: Proof. intros; apply Uplus_le_perm_left. apply Ole_trans with (mu m (fun x => g x + (f x - g x))). apply mu_monotonic; auto. apply (mu_le_plus m g (fun x => f x - g x)). Qed.
imports: ALEA(Monads) ALEA(Utheory)