proposition: Lemma fun_Lim_seq_minus : 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. set (F := Cauchy_fun_seq_Lim _ _ _ _ _ Hf) in *. cut (Continuous_I Hab F). intro H0. 2: unfold F in |- *; apply Cauchy_cont_Lim. cut (conv_fun_seq' _ _ _ _ _ contf H0). 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 H1. 2: unfold G in |- *; apply Cauchy_cont_Lim. cut (conv_fun_seq' _ _ _ _ _ contg H1). 2: unfold G in |- *; apply Cauchy_conv_fun_seq'; assumption. intro Hg'. apply fun_Lim_seq_minus' with contf contg H0 H1; auto. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval