proposition: Lemma mu_stable_mult_right : forall (A : Type)(m:distr A) (c:U) (f : MF A), mu m (fun x => (f x) * c) == (mu m f) * c.
proof: Proof. intros; apply Oeq_trans with (mu m (fun x => c * (f x))). apply mu_stable_eq; simpl; auto. apply Oeq_trans with (c * mu m f); auto. exact (mu_stable_mult m c f). Qed.
imports: ALEA(Monads) ALEA(Utheory)