proposition: Lemma is_lim_seq_scal_r (u : nat -> R) (a : R) (lu : Rbar) : is_lim_seq u lu -> is_lim_seq (fun n => u n * a) (Rbar_mult lu a).
proof: Proof. move => Hu Ha. apply is_lim_seq_ext with ((fun n : nat => a * u n)). move => n ; by apply Rmult_comm. rewrite Rbar_mult_comm. apply is_lim_seq_scal_l. by apply Hu. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy