proposition: Lemma Mmult_stable_mult : forall A (k:MF A) (d:distr A), stable_mult (Mmult k (mu d)).
proof: Proof. red; intros; simpl. apply Oeq_trans with (mu d (fmult k0 (fun x : A => k x * f x))). apply (mu_stable_eq d). simpl; apply ford_eq_intro; intro x; unfold fmult; auto. apply (mu_stable_mult d). Qed.
imports: ALEA(Monads) ALEA(Utheory)