proposition: Lemma is_lim_comp' : forall {T} {F} {FF : @Filter T F} (f : T -> R) (g : R -> R) (x l : Rbar), filterlim f F (Rbar_locally x) -> is_lim g x l -> F (fun y => Finite (f y) <> x) -> filterlim (fun y => g (f y)) F (Rbar_locally l).
proof: Proof. intros T F FF f g x l Lf Lg Hf. revert Lg. apply filterlim_comp. intros P HP. destruct x as [x| |] ; try now apply Lf. specialize (Lf _ HP). unfold filtermap in Lf |- *. generalize (filter_and _ _ Hf Lf). apply filter_imp. intros y [H Hi]. apply Hi. contradict H. now apply f_equal. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq