proposition: Lemma Rseq_cv_finite_plus_neg_infty_r : forall l, Rseq_cv Un l -> Rseq_cv_neg_infty Vn -> Rseq_cv_neg_infty (Un + Vn).
proof: Proof. intros l Hl Hf M. destruct (Hl 1 ltac:(lra)) as [N HN]. destruct (Hf (M-(l +1))%R) as [N0 HN0]. exists (N+N0)%nat. intros n Hn. apply Rlt_le_trans with ((l+1)+ (M-(l+1)))%R. apply Rplus_lt_compat. apply Rminus_lt. unfold Rminus. rewrite Ropp_plus_distr. rewrite <- Rplus_assoc. rewrite Rplus_comm. replace 0 with (-1 + 1)%R by ring. apply Rplus_lt_compat_l. apply Rle_lt_trans with (Rabs (Un n+ - l)). apply RRle_abs. apply HN; lia. apply HN0; lia. ring_simplify; apply Rle_refl. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra