proposition: Lemma is_lim_comp_lin (f : R -> R) (a b : R) (x l : Rbar) : is_lim f (Rbar_plus (Rbar_mult a x) b) l -> a <> 0 -> is_lim (fun y => f (a * y + b)) x l.
proof: Proof. move => Hf Ha. apply is_lim_comp with (Rbar_plus (Rbar_mult a x) b). by apply Hf. eapply is_lim_plus. apply is_lim_scal_l. apply is_lim_id. apply is_lim_const. apply Rbar_plus_correct. case: (Rbar_mult a x) => //. case: x {Hf} => [x | | ] //=. exists (mkposreal _ Rlt_0_1) => y _ Hy. apply Rbar_finite_neq, Rminus_not_eq ; ring_simplify (a * y + b - (a * x + b)). rewrite -Rmult_minus_distr_l. apply Rmult_integral_contrapositive ; split. by []. by apply Rminus_eq_contra. exists 0 => x Hx. apply sym_not_eq in Ha. case: Rle_dec => // H. case: Rle_lt_or_eq_dec => //. exists 0 => x Hx. apply sym_not_eq in Ha. case: Rle_dec => // H. case: Rle_lt_or_eq_dec => //. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq