proposition: Lemma Rseq_subseq_cv_pos_infty_compat : forall Un Vn, subsequence Un Vn -> Rseq_cv_pos_infty Vn -> Rseq_cv_pos_infty Un.
proof: Proof. intros Un Vn Hsub Hdv M. destruct (Hdv M) as [N HN]. exists N; intros n Hn. destruct Hsub as [phi Hphi]. rewrite Hphi. apply HN. apply Nat.le_trans with n. apply Hn. apply Rsubseq_n_le_extractor_n; destruct phi; auto. Qed.
imports: Reals Rsequence_def Rsequence_facts Lia Lra