proposition: Lemma Rser_partial_big_O_compat : forall (Un : nat -> R), Un = O(Vn) -> sum_f_R0 Un = O(sum_f_R0 Vn).
proof: Proof. intros Un HO. assert (forall n, 0<= Rabs(Un n)) as RUn_pos. intro n; apply Rabs_pos. destruct (Rser_big_O_maj Un Vn Vn_pos HO) as [K [SN [K_pos Hmaj]]]. destruct (Vn_infty SN) as [N HN]. exists (K+1)%R. split. auto with *. exists N; intros n Hn. apply Rle_trans with (K * sum_f_R0 Vn n + SN)%R. apply Rle_trans with (sum_f_R0 (fun k : nat => Rabs (Un k)) n). apply sum_f_R0_triangle. apply Hmaj. rewrite Rmult_plus_distr_r. rewrite Rabs_pos_eq. ring_simplify. apply Rplus_le_compat_l. apply Rlt_le; apply HN; apply Hn. apply (cond_pos_sum _ _ 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