proposition: Lemma Rseq_cv_little_O_cv_pos_infty : (Rseq_cv Un l) -> (Rseq_cv_pos_infty Vn) -> Un = o(Vn).
proof: Proof. intros Un_cv Vn_cv_pos_infty eps epspos. destruct (Rseq_cv_bound Un l Un_cv) as [M [Mpos Mbound]]. destruct (Vn_cv_pos_infty (M/eps)%R) as [N Vnlowerbound]. exists N. intros n HnN. apply Rle_trans with M. apply Mbound. apply Rlt_le. assert (REW : (M = eps * (M / eps))%R). field. intro zero; subst; apply (Rlt_irrefl _ epspos). rewrite REW. apply Rmult_lt_compat_l; [assumption|]. apply Rlt_le_trans with (Vn n). apply (Vnlowerbound _ HnN). apply RRle_abs. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra