proposition: Lemma is_lim_seq_subseq (u : nat -> R) (l : Rbar) (phi : nat -> nat) : filterlim phi eventually eventually -> is_lim_seq u l -> is_lim_seq (fun n => u (phi n)) l.
proof: Proof. intros Hphi. now apply filterlim_comp. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy