proposition: Lemma Rseq_cv_finite_minus_neg_infty : forall l, Rseq_cv Un l -> Rseq_cv_neg_infty Vn -> Rseq_cv_pos_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 Rle_lt_trans with ((l-1)+ -(-M+(l -1)))%R. ring_simplify; apply Rle_refl. apply Rplus_lt_compat. apply Rminus_lt. unfold Rminus. rewrite Rplus_comm. 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. rewrite Rplus_comm. fold (Rminus l (Un n)). fold (R_dist l (Un n)). rewrite R_dist_sym. apply HN; lia. apply Ropp_gt_lt_contravar. apply HN0; lia. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra