proposition: Lemma Lim_comp_lin (f : R -> R) (a b : R) (x : Rbar) : ex_lim f (Rbar_plus (Rbar_mult a x) b) -> a <> 0 -> Lim (fun y => f (a * y + b)) x = Lim f (Rbar_plus (Rbar_mult a x) b).
proof: Proof. move => Hf Ha. apply is_lim_unique. apply is_lim_comp_lin. by apply Lim_correct. exact: Ha. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq