proposition: Lemma ex_lim_seq_scal_r (u : nat -> R) (a : R) : ex_lim_seq u -> ex_lim_seq (fun n => u n * a).
proof: Proof. move => Hu. apply ex_lim_seq_ext with ((fun n : nat => a * u n)) ; try by intuition. apply ex_lim_seq_scal_l. by apply Hu. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy