proposition: Lemma Rseq_equiv_eq_compat : forall Un Vn Wn Xn, Un == Wn -> Vn == Xn -> Un ~ Vn -> Wn ~ 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. unfold Rseq_minus. rewrite <- Huw; rewrite <- Hvx. apply HN; apply Hn. Qed.
imports: Lia Rsequence_def Morphisms Setoid Lra