proposition: Lemma is_lim_comp_seq (f : R -> R) (u : nat -> R) (x l : Rbar) : is_lim f x l -> eventually (fun n => Finite (u n) <> x) -> is_lim_seq u x -> is_lim_seq (fun n => f (u n)) l.
proof: Proof. intros Lf Hu Lu. exact (is_lim_comp' u f x l Lu Lf Hu). Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq