proposition: Lemma Rseq_cv_pos_infty_asymptotic : Rseq_asymptotic Rseq_cv_pos_infty.
proof: Proof. intros Q Un HQ He M. destruct He as [Ne HNe]. edestruct HQ as [N HN]; [eexact HNe|]. exists (Ne + N)%nat; intros n Hn. assert (Hn0 : exists n0, (n = Ne + n0)%nat). induction Hn. exists N; reflexivity. destruct IHHn as [n0 H]; exists (S n0). rewrite <- Nat.add_succ_comm; simpl; rewrite H; reflexivity. destruct Hn0 as [n0 Hn0]. rewrite Hn0; apply HN; lia. Qed.
imports: Lia Rsequence_def Morphisms Setoid Lra