proposition: Lemma Lim_scal_r (f : R -> R) (a : R) (x : Rbar) : Lim (fun y => f y * a) x = Rbar_mult (Lim f x) a.
proof: Proof. rewrite Rbar_mult_comm -Lim_seq_scal_l. apply Lim_seq_ext. move => y ; by apply Rmult_comm. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq