proposition: Lemma serie_fun_lub_sigma_fun : forall A (f:nat -> MF A), serie_fun f == lub (c:=MF A) (Sigma_fun f).
proof: Proof. intros; unfold serie_fun. simpl; apply ford_eq_intro; intro x. unfold serie; apply lub_eq_compat. simpl; apply fmon_eq_intro; intro n; trivial. Qed.
imports: ALEA(Monads) ALEA(Utheory)