proposition: Lemma serie_sigma_lift : forall (f :nat -> U) (n:nat), serie f == sigma f n + serie (fun k => f (n + k)%nat).
proof: Proof. intros f n; unfold serie; apply Oeq_trans with (lub (mseq_lift_left (sigma f) n)); auto. apply Oeq_trans with (lub (UPlus (sigma f n) @ sigma (fun k => f (n+k)%nat))). apply lub_eq_compat; apply fmon_eq_intro; intros. rewrite mseq_lift_left_simpl. rewrite fmon_comp_simpl. apply (sigma_plus_lift f n n0). symmetry. apply (lub_comp_eq (f:=UPlus (sigma f n)) (sigma (fun k : nat => f (n + k)%nat)) ). apply (continuous2_app Uplus_continuous2). Qed.
imports: ALEA(Utheory)