proposition: Lemma Rseq_cv_finite_minus_pos_infty : forall l, Rseq_cv Un l -> Rseq_cv_pos_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 ((l +1)+ -M)%R) as [N0 HN0]. exists (N+N0)%nat. intros n Hn. apply Rlt_le_trans with ((l+1)+ -((l +1)+-M))%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 Ropp_gt_lt_contravar. apply HN0; lia. ring_simplify; apply Rle_refl. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra