proposition: Lemma limit_plus : forall (f g:C -> C) (D:C -> Prop) (l l' z:C), limit1_in f D l z -> limit1_in g D l' z -> limit1_in (fun x:C => f x + g x) D (l + l') z.
proof: Proof. intros; unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; intros; elim (H (eps * / 2)%R (eps2_Rgt_R0 eps H1)); elim (H0 (eps * / 2)%R (eps2_Rgt_R0 eps H1)); simpl in |- *; clear H H0; intros; elim H; elim H0; clear H H0; intros; split with (Rmin x0 x); split. apply Rmin_Rgt_r ; split ; assumption. intros; elim H4; clear H4; intros; cut (C_dist (f x1) l + C_dist (g x1) l' < eps). cut (C_dist (f x1 + g x1) (l + l') <= C_dist (f x1) l + C_dist (g x1) l'). apply Rle_lt_trans. apply C_dist_plus. elim (Rmin_Rgt_l x0 x (C_dist x1 z) H5); clear H5; intros. generalize (H3 x1 (conj H4 H6)); generalize (H0 x1 (conj H4 H5)); intros; replace eps with (eps * / 2 + eps * / 2)%R. apply Rplus_lt_compat ; assumption. apply eps2. Qed.
imports: Rlimit Cbase Ctacfield Cnorm Cprop_base Rsequence_def Csequence Csequence_facts Cfunctions