proposition: Lemma Rseq_little_O_plus_compat_l : Un = o(Wn) -> Vn = o(Wn) -> (Un + Vn) = o(Wn).
proof: Proof. intros Hu Hv. intros eps Heps. destruct (Hu (eps/2)%R) as [Nu HNu]; [lra|]. destruct (Hv (eps/2)%R) as [Nv HNv]; [lra|]. exists (Nat.max Nu Nv). intros n Hn. unfold Rseq_plus. eapply Rle_trans; [apply Rabs_triang|]. replace eps with (eps / 2 + eps / 2)%R by field. rewrite Rmult_plus_distr_r. apply Rplus_le_compat. apply (HNu n); eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. apply (HNv n); eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra