proposition: Lemma Lim_seq_subseq (u : nat -> R) (phi : nat -> nat) : filterlim phi eventually eventually -> ex_lim_seq u -> Lim_seq (fun n => u (phi n)) = Lim_seq u.
proof: Proof. move => Hphi Hu. apply is_lim_seq_unique. apply is_lim_seq_subseq. exact Hphi. by apply Lim_seq_correct. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy