proposition: Lemma Rseq_cv_asymptotic_eq_compat : forall Un Vn l, (exists N, forall n : nat, (N <= n)%nat -> Un n = Vn n) -> Rseq_cv Un l -> Rseq_cv Vn l.
proof: Proof. intros Un Vn l [N HN] Hu eps Heps. destruct (Hu eps Heps) as [N' HN']. exists (N+N')%nat. intros n Hn; unfold R_dist. replace (Vn n -l)%R with ((Vn n - Un n) + (Un n -l))%R by ring. apply Rle_lt_trans with (Rabs (Vn n - Un n)+ Rabs(Un n -l))%R. apply Rabs_triang. rewrite HN at 1. unfold Rminus at 1. rewrite Rplus_opp_r, Rabs_R0, Rplus_0_l. apply HN'. lia. lia. Qed.
imports: Lia Rsequence_def Morphisms Setoid Lra