proposition: Lemma is_lim_comp (f g : R -> R) (x k l : Rbar) : is_lim f l k -> is_lim g x l -> Rbar_locally' x (fun y => Finite (g y) <> l) -> is_lim (fun x => f (g x)) x k.
proof: Proof. intros Lf Lg Hg. by apply (is_lim_comp' g f l k Lg Lf Hg). Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq