proposition: Lemma Rseq_cv_eq_compat : forall Un Vn l, Un == Vn -> (Rseq_cv Un l <-> Rseq_cv Vn l).
proof: Proof. intros Un Vn l Heq ; split ; intros Hcv eps Heps ; destruct (Hcv eps Heps) as [N HN] ; exists N; intros n Hn ; [rewrite <- Heq | rewrite Heq] ; apply HN; assumption. Qed.
imports: Lia Rsequence_def Morphisms Setoid Lra