proposition: Lemma Rseq_equiv_little_O_compat_l : forall Un Vn Wn, Un ~ Vn -> Un = o(Wn) -> Vn = o(Wn).
proof: Proof. intros Un Vn Wn He Ho eps Heps. pose (eps' := Rmin 1 eps). assert (Heps' : eps' > 0). unfold eps'; unfold Rmin; destruct Rle_dec; lra. destruct (He (eps' / 2)%R) as [Ne HNe]; [lra|]. destruct (Ho (eps' / 2)%R) as [No HNo]; [lra|]. exists (Nat.max Ne No); intros n Hn. replace (Vn n) with (Vn n - Un n + Un 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. rewrite Rabs_minus_sym. eapply Rle_trans. apply HNe; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. eapply Rle_trans with (eps / 2 * Rabs (Un n))%R. apply Rmult_le_compat_r; [apply Rabs_pos|]. unfold eps'; unfold Rmin; destruct Rle_dec; lra. apply Rmult_le_compat_l; [lra|]. eapply Rle_trans. apply HNo; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. rewrite <- Rmult_1_l. apply Rmult_le_compat_r; [apply Rabs_pos|]. rewrite <- Rmult_1_l. apply Rmult_le_compat; try lra; apply Rmin_l. eapply Rle_trans. apply HNo; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. apply Rmult_le_compat_r; [apply Rabs_pos|]. apply Rmult_le_compat_r; [lra|apply Rmin_r]. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra