proposition: Lemma fun_Lim_seq_plus : forall H H', conv_fun_seq' a b Hab (fun n => f n{+}g n) (Cauchy_fun_seq_Lim _ _ _ _ _ Hf{+}Cauchy_fun_seq_Lim _ _ _ _ _ Hg) H H'.
proof: Proof. intros H H' e H0. set (F := Cauchy_fun_seq_Lim _ _ _ _ _ Hf) in *. cut (Continuous_I Hab F). intro H1. 2: unfold F in |- *; apply Cauchy_cont_Lim. cut (conv_fun_seq' _ _ _ _ _ contf H1). 2: unfold F in |- *; apply Cauchy_conv_fun_seq'; assumption. intro Hf'. set (G := Cauchy_fun_seq_Lim _ _ _ _ _ Hg) in *. cut (Continuous_I Hab G). intro H2. 2: unfold G in |- *; apply Cauchy_cont_Lim. cut (conv_fun_seq' _ _ _ _ _ contg H2). 2: unfold G in |- *; apply Cauchy_conv_fun_seq'; assumption. intro Hg'. apply fun_Lim_seq_plus' with contf contg H1 H2; auto. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval