proposition: Lemma Rseq_equiv_plus_little_O_compat_l : Un ~ Wn -> En = o(Un) -> (Un + En) ~ Wn.
proof: Proof. intros Hu Ho. apply Rseq_equiv_sym; apply Rseq_equiv_sym in Hu. intros eps Heps. assert (Hpos : (eps * / (2 + eps) > 0)%R). apply Rmult_lt_0_compat; [lra|]. apply Rinv_0_lt_compat; lra. destruct (Hu (eps / 2)%R) as [N HN]; [lra|]. destruct (Ho (eps * / (2 + eps))%R) as [No HNo]; [assumption|]. exists (Nat.max N No); intros n Hn. unfold Rseq_plus; unfold Rseq_minus. replace (Wn n - (Un n + En n))%R with (Wn n + - Un n + - En n)%R by field. replace eps with (eps / 2 + eps / 2)%R by field. eapply Rle_trans; [apply Rabs_triang|]. rewrite Rmult_plus_distr_r; apply Rplus_le_compat. apply HN; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. rewrite Rabs_Ropp. eapply Rle_trans. apply HNo; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. replace (Un n) with (Un n - Wn n + Wn n)%R by field. eapply Rle_trans. apply Rmult_le_compat_l; [left; assumption|apply Rabs_triang]. eapply Rle_trans. apply Rmult_le_compat_l; [left; assumption|]. apply Rplus_le_compat_r. rewrite Rabs_minus_sym. apply HN; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. right; field; apply Rgt_not_eq; lra. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra