proposition: Lemma ex_lim_comp_lin (f : R -> R) (a b : R) (x : Rbar) : ex_lim f (Rbar_plus (Rbar_mult a x) b) -> ex_lim (fun y => f (a * y + b)) x.
proof: Proof. case => l Hf. case: (Req_dec a 0) => [-> {a Hf} | Ha]. apply ex_lim_ext with (fun _ => f b). move => y ; by rewrite Rmult_0_l Rplus_0_l. by apply ex_lim_const. exists l ; by apply is_lim_comp_lin. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq