proposition: Lemma Rseq_equiv_big_O_compat_r : forall Un Vn Wn, Un ~ Vn -> Wn = O(Un) -> Wn = O(Vn).
proof: Proof. intros Un Vn Wn He HO. apply Rseq_equiv_sym in He. destruct HO as [M [HM [NO HNO]]]. destruct (He 1) as [Ne HNe]; [lra|]. exists (M * 2)%R; split; [lra|]. exists (Nat.max Ne NO); intros n Hn. eapply Rle_trans. apply HNO; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. rewrite Rmult_assoc. apply Rmult_le_compat_l; [lra|]. replace (Un n) with (Un n - Vn n + Vn n)%R by field. eapply Rle_trans; [apply Rabs_triang|]. change 2 with (1 + 1)%R. rewrite Rmult_plus_distr_r. apply Rplus_le_compat. rewrite Rabs_minus_sym. apply HNe; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. rewrite Rmult_1_l; apply Rle_refl. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra