proposition: Lemma Cauchy_Lim_plus : forall seq1 seq2 y1 y2, Cauchy_Lim_prop2 seq1 y1 -> Cauchy_Lim_prop2 seq2 y2 -> Cauchy_Lim_prop2 (fun n => seq1 n [+] seq2 n) (y1 [+] y2).
proof: Proof. intros seq1 seq2 y1 y2 H H0. unfold Cauchy_Lim_prop2 in |- *. intros eps H1. cut ([0] [<] eps [/]TwoNZ). intro H2. elim (H _ H2); intros x H3. elim (H0 _ H2); intros x0 H4. exists (Nat.max x x0). intros. rstepr (seq1 m[-]y1[+] (seq2 m[-]y2)). apply AbsSmall_eps_div_two. apply H3. apply Nat.le_trans with (Nat.max x x0). apply Nat.le_max_l. assumption. apply H4. apply Nat.le_trans with (Nat.max x x0). apply Nat.le_max_r. assumption. apply pos_div_two. assumption. Qed.
imports: CoRN.reals.CReals Coq(Lia)