proposition: Lemma Lim_scal_l (f : R -> R) (a : R) (x : Rbar) : Lim (fun y => a * f y) x = Rbar_mult a (Lim f x).
proof: Proof. apply Lim_seq_scal_l. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq