proposition: Lemma Mmult_stable_plus : forall A (k:MF A) (d:distr A), stable_plus (Mmult k (mu d)).
proof: Proof. red; intros; simpl. apply Oeq_trans with (mu d (fun x => k x * f x + k x * g x)). apply (mu_stable_eq d). simpl; apply ford_eq_intro; intro x; unfold fplus. apply Udistr_plus_left; apply (H x). apply (mu_stable_plus d (f:=fun x=> k x * f x) (g:=fun x => k x * g x)). intro x; apply Ole_trans with (f x); auto. apply Ole_trans with (finv g x); auto. unfold finv; repeat Usimpl; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)