proposition: Lemma mu_stable_minus : forall (A:Type) (m:distr A)(f g : MF A), g <= f -> mu m (fun x => f x - g x) == mu m f - mu m g.
proof: Proof. intros; change (mu m (fminus f g) == mu m f - mu m g). apply (stable_minus_distr (m:=mu m)); auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)