proposition: Lemma Rseq_little_O_cv_pos_infty : Rseq_cv_pos_infty Un -> Rseq_cv_pos_infty (|Vn|).
proof: Proof. intros H M. destruct (H M) as [N HN]. destruct (Ho 1) as [No HNo]; [lra|]. exists (Nat.max N No); intros n Hn. eapply Rlt_le_trans. apply (HN n); eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. rewrite <- Rmult_1_l. apply Rle_trans with (Rabs (Un n)). unfold Rabs; repeat destruct Rcase_abs; lra. apply HNo; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra