proposition: Lemma limit_plus : forall (f g:R -> R) (D:R -> Prop) (l l' x0:R), limit1_in f D l x0 -> limit1_in g D l' x0 -> limit1_in (fun x:R => f x + g x) D (l + l') x0.
proof: Proof. intros; unfold limit1_in; unfold limit_in; simpl; intros; elim (H (eps * / 2) (eps2_Rgt_R0 eps H1)); elim (H0 (eps * / 2) (eps2_Rgt_R0 eps H1)); simpl; clear H H0; intros; elim H; elim H0; clear H H0; intros; split with (Rmin x1 x); split. - exact (Rmin_Rgt_r x1 x 0 (conj H H2)). - intros; elim H4; clear H4; intros; cut (Rdist (f x2) l + Rdist (g x2) l' < eps). + cut (Rdist (f x2 + g x2) (l + l') <= Rdist (f x2) l + Rdist (g x2) l'). * exact (Rle_lt_trans _ _ _). * exact (Rdist_plus _ _ _ _). + elim (Rmin_Rgt_l x1 x (Rdist x2 x0) H5); clear H5; intros. generalize (H3 x2 (conj H4 H6)); generalize (H0 x2 (conj H4 H5)); intros; replace eps with (eps * / 2 + eps * / 2). * exact (Rplus_lt_compat _ _ _ _ H7 H8). * exact (eps2 eps). Qed.
imports: Rbase Rfunctions Lra