proposition: Corollary Rseq_even_growing_compat : forall un l, Rseq_growing un -> Rseq_cv (fun i => un (2*i)%nat) l -> Rseq_cv un l.
proof: Proof. intros. apply Rseq_subseq_growing_cv_compat with (fun i : nat => un (2 * i)%nat). assert (Hex : is_extractor (mult 2)). intros n; lia. pose (phi := exist _ (mult 2) Hex). exists phi; reflexivity. assumption. assumption. Qed.
imports: Reals Rsequence_def Rsequence_facts Lia Lra