proposition: Lemma serie_plus : forall (f g : nat -> U), serie (fun k => (f k) + (g k)) == serie f + serie g.
proof: Proof. intros; unfold serie. apply Oeq_trans with (lub ((UPlus @2 sigma f) (sigma g))); auto. apply lub_eq_compat; apply fmon_eq_intro; intro n. exact (sigma_plus f g n). Qed.
imports: ALEA(Utheory)