proposition: Lemma ex_lim_scal_l (f : R -> R) (a : R) (x : Rbar) : ex_lim f x -> ex_lim (fun y => a * f y) x.
proof: Proof. case => l Hf. exists (Rbar_mult a l). by apply is_lim_scal_l. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq