proposition: Lemma CV_plus : forall (An Bn:nat -> R) (l1 l2:R), Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i + Bn i) (l1 + l2).
proof: Proof. unfold Un_cv; unfold Rdist; intros. cut (0 < eps / 2); [ intro | unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. elim (H (eps / 2) H2); intros. elim (H0 (eps / 2) H2); intros. set (N := max x x0). exists N; intros. replace (An n + Bn n - (l1 + l2)) with (An n - l1 + (Bn n - l2)); [ idtac | ring ]. apply Rle_lt_trans with (Rabs (An n - l1) + Rabs (Bn n - l2)). - apply Rabs_triang. - rewrite <-(Rplus_half_diag eps); apply Rplus_lt_compat. + apply H3; unfold ge; apply Nat.le_trans with N; [ unfold N; apply Nat.le_max_l | assumption ]. + apply H4; unfold ge; apply Nat.le_trans with N; [ unfold N; apply Nat.le_max_r | assumption ]. Qed.
imports: Rbase Rfunctions Rseries Lia