proposition: Lemma is_lim_seq_continuous (f : R -> R) (u : nat -> R) (l : R) : continuity_pt f l -> is_lim_seq u l -> is_lim_seq (fun n => f (u n)) (f l).
proof: Proof. move => Cf Hu. apply continuity_pt_filterlim in Cf. apply filterlim_comp with (1 := Hu). exact Cf. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy