proposition: Lemma Rseq_cv_pos_infty_eq_compat : forall Un Vn, Un == Vn -> Rseq_cv_pos_infty Un -> Rseq_cv_pos_infty Vn.
proof: Proof. intros Un Vn Heq Hdiv. intros m. destruct (Hdiv m) as [N HN]. exists N; intros n Hn. rewrite <- (Heq n). apply HN; assumption. Qed.
imports: Lia Rsequence_def Morphisms Setoid Lra