proposition: Lemma is_lim_scal_l (f : R -> R) (a : R) (x l : Rbar) : is_lim f x l -> is_lim (fun y => a * f y) x (Rbar_mult a l).
proof: Proof. move => Hf. case: (Req_dec 0 a) => [<- {a} | Ha]. rewrite Rbar_mult_0_l. apply is_lim_ext with (fun _ => 0). move => y ; by rewrite Rmult_0_l. by apply is_lim_const. apply is_lim_mult. by apply is_lim_const. by apply Hf. apply sym_not_eq in Ha. case: l {Hf} => [l | | ] //=. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq