proposition: Lemma Rseq_little_O_eq_compat : forall Un Vn Wn Xn, Un == Wn -> Vn == Xn -> Un = o(Vn) -> Wn = o(Xn).
proof: Proof. intros Un Vn Wn Xn Huw Hvx Huv. intros eps Heps. destruct (Huv eps Heps) as [N HN]. exists N; intros n Hn. rewrite <- Huw; rewrite <- Hvx. apply HN; assumption. Qed.
imports: Lia Rsequence_def Morphisms Setoid Lra