proposition: Lemma is_lim_comp_continuous (f g : R -> R) (x : Rbar) (l : R) : is_lim f x l -> continuous g l -> is_lim (fun x => g (f x)) x (g l).
proof: Proof. intros Hf Hg. apply filterlim_locally => eps. destruct (proj1 (filterlim_locally _ _) Hg eps) as [e He] ; clear Hg. eapply filter_imp. intros y Hy. apply He, Hy. by apply Hf, locally_ball. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq