proposition: Lemma Rseq_cv_abs_compat : forall (Un : nat -> R) (l : R), Rseq_cv Un l -> Rseq_cv (|Un|) (Rabs l).
proof: Proof. intros Un l Hl eps Heps. destruct (Hl eps Heps) as [N HN]. exists N. intros n Hn. unfold R_dist. apply Rle_lt_trans with (Rabs (Un n - l)). apply Rabs_triang_inv2. apply HN; apply Hn. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra