proposition: Lemma Rser_partial_little_O_compat : forall (Un : nat -> R), Un = o(Vn) -> sum_f_R0 Un = o(sum_f_R0 Vn).
proof: Proof. intros Un Ho eps Heps. assert (0<eps/2) as Heps2; [lra|]. destruct (Rser_little_O_maj _ _ Vn_pos Ho (eps /2)) as [C HC]. apply Heps2. destruct (Vn_infty (C/(eps/2))%R) as [N HN]. exists N. intros n Hn. rewrite Rabs_pos_eq with (sum_f_R0 Vn n). apply Rle_trans with (sum_f_R0 (fun k : nat => Rabs (Un k)) n). apply sum_f_R0_triangle. apply Rle_trans with ((eps / 2) * sum_f_R0 Vn n + C)%R. apply HC. rewrite double_var with eps . rewrite <- double_var at 1. rewrite Rmult_plus_distr_r. apply Rplus_le_compat_l. assert (C = (eps/2)*(/(eps/2))*C)%R as HCr. field. intro Hf; apply Rlt_irrefl with 0; rewrite Hf in Heps; apply Heps. rewrite HCr. rewrite Rmult_assoc. apply Rmult_le_compat_l. apply Rlt_le; apply Heps2. rewrite Rmult_comm. apply Rlt_le. apply HN; apply Hn. apply (cond_pos_sum Vn n Vn_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