proposition: Lemma is_lim_scal_r (f : R -> R) (a : R) (x l : Rbar) : is_lim f x l -> is_lim (fun y => f y * a) x (Rbar_mult l a).
proof: Proof. move => Hf. rewrite Rbar_mult_comm. apply is_lim_ext with (fun y => a * f y). move => y ; by apply Rmult_comm. by apply is_lim_scal_l. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq