proposition: Lemma Rser_rem_little_O_compat : Un = o(Vn) -> (Rser_rem Un lu Hlu) = o(Rser_rem Vn lv Hlv).
proof: Proof. intros Ho eps Heps. destruct (Ho eps Heps) as [N HN]. exists N. intros n Hn. assert (0<= eps) as eps_pos. apply Rlt_le; apply Heps. rewrite <- Rabs_pos_eq with eps. rewrite <- Rabs_mult. apply Rle_cv_lim with (fun p : nat => Rabs (sum_f_R0 (fun k => (Un (S n+k))) p))%R (fun p : nat => Rabs (sum_f_R0 (fun k => (Vn (S n+k))*eps) p))%R. intro p. apply Rle_trans with (sum_f_R0 (fun k : nat =>(Rabs (Un (S n + k)))) p)%R. apply Rabs_triang_gen. rewrite Rabs_pos_eq. apply sum_Rle. intros k Hk. rewrite <- Rabs_pos_eq with (Vn (S n + k)). rewrite Rmult_comm. apply HN; lia. apply Vn_pos. apply cond_pos_sum; intro. apply Rmult_le_pos; [ apply Vn_pos| apply eps_pos]. apply Rseq_cv_abs_compat; apply Rser_rem_cv. apply Rseq_cv_abs_compat. apply Rseq_cv_eq_compat with (fun p : nat => eps * sum_f_R0 (fun k : nat => ( Vn (S n + k))) p)%R. intro; rewrite (scal_sum _ _ eps); reflexivity. apply CV_mult. apply Rseq_constant_cv. apply Rser_rem_cv. apply eps_pos. Qed.
imports: Reals Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts Rseries_remainder_facts Rseries_cv_facts Rseries_usual Lra PeanoNat Rtactic MyRIneq