proposition: Lemma Rseq_little_O_cv : Rseq_cv Vn l -> Rseq_cv Un 0.
proof: Proof. intros H eps Heps. assert (Hpos : / (1 + Rabs l) > 0). apply Rinv_0_lt_compat. eapply Rlt_le_trans with (r2 := 1); [lra|]. pattern 1 at 1; rewrite <- Rplus_0_r. apply Rplus_le_compat_l; apply Rabs_pos. destruct (H 1) as [Ncv HNcv]; [lra|]. destruct (Ho (/ (1 + Rabs l) * eps))%R as [No HNo]. apply Rmult_gt_0_compat; assumption. exists (Nat.max Ncv No). intros n Hn. unfold R_dist; rewrite Rminus_0_r. eapply Rle_lt_trans; [apply HNo|]. eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. rewrite Rmult_comm; rewrite <- Rmult_assoc. rewrite <- Rmult_1_l; apply Rmult_lt_compat_r; [assumption|]. eapply Rlt_le_trans. apply Rmult_lt_compat_r; [assumption|]. replace (Vn n) with (Vn n - l + l)%R by field. eapply Rle_lt_trans. apply Rabs_triang. apply Rplus_lt_compat_r. apply HNcv; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. right; apply Rinv_r; apply Rgt_not_eq. eapply Rlt_le_trans with (r2 := 1); [lra|]. pattern 1 at 1; rewrite <- Rplus_0_r. apply Rplus_le_compat_l; apply Rabs_pos. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra