proposition: Lemma Rseq_cv_neg_minus_pos_infty : Rseq_cv_neg_infty Un -> Rseq_cv_pos_infty Vn -> Rseq_cv_neg_infty (Un - Vn).
proof: Proof. intros Hl Hf M. destruct (Hl M) as [N HN]. destruct (Hf 0%R) as [N0 HN0]. exists (N+N0)%nat. intros n Hn. apply Rlt_le_trans with (M+-0)%R. apply Rplus_lt_compat. 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