proposition: Lemma Rseq_big_O_plus_compat_l : Un = O(Wn) -> Vn = O(Wn) -> (Un + Vn) = O(Wn).
proof: Proof. intros Hu Hv. destruct Hu as [Mu [HMu [Nu Hu]]]. destruct Hv as [Mv [HMv [Nv Hv]]]. exists (Mu + Mv)%R; split; [lra|]. exists (Nat.max Nu Nv). intros n Hn. unfold Rseq_plus. eapply Rle_trans; [apply Rabs_triang|]. rewrite Rmult_plus_distr_r. apply Rplus_le_compat. apply (Hu n); eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. apply (Hv 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