proposition: Lemma Rseq_equiv_little_O_compat_r : forall Un Vn Wn, Un ~ Vn -> Wn = o(Un) -> Wn = o(Vn).
proof: Proof. intros Un Vn Wn He Ho eps Heps. apply Rseq_equiv_sym in He. pose (eps1 := (eps / (2 + eps))%R). pose (eps2 := (eps / 2)%R). assert (Heps1 : eps1 > 0). unfold eps1; unfold Rdiv; apply Rmult_lt_0_compat; [|apply Rinv_0_lt_compat]; lra. assert (Heps2 : eps2 > 0). unfold eps2; lra. destruct (Ho eps1) as [No HNo]; [assumption|]. destruct (He eps2) as [Ne HNe]; [assumption|]. exists (Nat.max No Ne); intros n Hn. eapply Rle_trans. apply HNo; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. unfold eps1; unfold Rdiv. rewrite Rmult_assoc; apply Rmult_le_compat_l; [lra|]. rewrite <- Rmult_1_l. pattern 1 at 1. replace 1%R with (/ (2 + eps) * (2 + eps))%R by (field; apply Rgt_not_eq; lra). rewrite Rmult_assoc; apply Rmult_le_compat_l. left; apply Rinv_0_lt_compat; lra. replace (Un n) with (Un n - Vn n + Vn n)%R by field. replace (2 + eps)%R with (eps + 1 + 1)%R by field. eapply Rle_trans; [apply Rabs_triang|]. rewrite Rmult_plus_distr_r; rewrite Rmult_1_l. apply Rplus_le_compat_r. rewrite Rabs_minus_sym. eapply Rle_trans. apply HNe; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. apply Rmult_le_compat_r; [apply Rabs_pos|]. unfold eps2; lra. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra