proposition: Lemma Rseq_subseq_growing_cv_compat : forall Un Vn l, subsequence Un Vn -> Rseq_cv Un l -> Rseq_growing Vn -> Rseq_cv Vn l.
proof: Proof. intros un vn l [phi ephi] uncv vngrow eps epspos. destruct phi as [phi Hphi]; unfold extracted in *; simpl in *. assert (spliteps : (eps / 3 > 0)%R) by lra. destruct (uncv (eps / 3) spliteps) as [Nu Hu]. exists (phi Nu). intros n nNu. destruct (Rseq_extractor_partition phi Hphi n) as [N Hpart]. apply Nat.le_trans with (phi Nu). apply nat_seq_growing_trans. intros x. apply Nat.lt_le_incl. apply Hphi. apply Nat.le_0_l. exact nNu. assert (HNuN : (Nu <= N)%nat). destruct (le_le_S_dec Nu N) as [goal|Hinv]. exact goal. destruct Hpart as [HNn HnSN]. pose proof (nat_seq_growing_trans phi (fun x => Nat.lt_le_incl _ _ (Hphi _)) Nu (S N) Hinv). pose proof (Nat.le_trans _ _ _ H nNu). pose proof (Nat.lt_le_trans _ _ _ HnSN H). intuition lia. pose proof (Hu N HNuN) as Hun. pose proof (Hu (S N) (le_S _ _ HNuN)) as Husn. rewrite ephi in Hun. rewrite ephi in Husn. assert (vn (phi N) <= vn n <= vn (phi (S N)))%R. split; apply (Rseq_growing_trans _ vngrow); intuition (auto with arith). rewrite R_dist_sym in Husn. replace eps with (eps / 3 + eps / 3 + eps / 3) by field. eapply Rle_lt_trans. apply (R_dist_tri _ _ (vn (phi (S N)))). apply Rplus_lt_compat. eapply R_dist_bounded_in_segment. apply H. eapply Rle_lt_trans. apply (R_dist_tri _ _ l). apply Rplus_lt_compat. apply Hun. apply Husn. rewrite R_dist_sym . apply Husn. Qed.
imports: Reals Rsequence_def Rsequence_facts Lia Lra