proposition: Lemma mu_serie_le : forall A (d:distr A) (f:nat -> MF A), mu d (serie_fun f) <= serie (fun k => mu d (f k)).
proof: Proof. intros; apply Ole_trans with (mu d (lub (Sigma_fun f))). apply mu_monotonic; rewrite (serie_fun_lub_sigma_fun f); trivial. apply Ole_trans with (lub (mu d @ (Sigma_fun f))). apply (mu_continuous d). unfold serie; apply lub_le_compat; intro n. rewrite fmon_comp_simpl. exact (mu_sigma_le d f n). Qed.
imports: ALEA(Monads) ALEA(Utheory)