proposition: Lemma mu_sigma_le : forall A (d:distr A) (f:nat -> MF A) (n:nat), mu d (sigma_fun f n) <= sigma (fun k => mu d (f k)) n.
proof: Proof. induction n; intros. rewrite sigma_0; apply Ole_trans with (mu d (fzero A)); auto. rewrite sigma_S; apply Ole_trans with (mu d (fplus (f n) (sigma_fun f n))). auto. apply Ole_trans with (mu d (f n) + mu d (sigma_fun f n)); auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)