proposition: Lemma is_lim_seq_scal_l (u : nat -> R) (a : R) (lu : Rbar) : is_lim_seq u lu -> is_lim_seq (fun n => a * u n) (Rbar_mult a lu).
proof: Proof. intros Hu H. apply filterlim_comp with (1 := Hu). by apply filterlim_Rbar_mult_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy