proposition: Lemma mu_serie_eq : forall A (d:distr A) (f:nat -> MF A), (forall x, wretract (fun k => f k x)) -> mu d (serie_fun f) == serie (fun k => mu d (f k)).
proof: Proof. intros; apply Oeq_trans with (mu d (lub (Sigma_fun f))). apply mu_stable_eq; apply (serie_fun_lub_sigma_fun f); trivial. apply Oeq_trans with (lub (mu d @ (Sigma_fun f))). apply (lub_comp_eq (f:=mu d)). apply (mu_continuous d). unfold serie; apply lub_eq_compat; apply fmon_eq_intro; intro n. rewrite fmon_comp_simpl. apply (mu_sigma_eq d f (n:=n)). red; intros. apply (H x k). Qed.
imports: ALEA(Monads) ALEA(Utheory)