proposition: Lemma Lim_comp (f g : R -> R) (x : Rbar) : ex_lim f (Lim g x) -> ex_lim g x -> Rbar_locally' x (fun y => Finite (g y) <> Lim g x) -> Lim (fun x => f (g x)) x = Lim f (Lim g x).
proof: Proof. intros. apply is_lim_unique. apply is_lim_comp with (Lim g x). by apply Lim_correct. by apply Lim_correct. by apply H1. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq