proposition: Lemma Rseq_subseq_cv_compat : forall Un Vn l, subsequence Un Vn -> Rseq_cv Vn l -> Rseq_cv Un l.
proof: Proof. intros Un Vn l Hsub Hcv eps Heps. destruct (Hcv eps Heps) as [N HN]. exists N; intros n Hn. destruct Hsub as [phi Hphi]. unfold extracted in *; simpl in 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