proposition: Lemma Rseq_big_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. destruct Huv as [M [HM [N HN]]]. exists M; split. assumption. exists N; intros n Hn. rewrite <- Huw; rewrite <- Hvx. apply HN; assumption. Qed.
imports: Lia Rsequence_def Morphisms Setoid Lra