proposition: Lemma ex_lim_seq_scal_l (u : nat -> R) (a : R) : ex_lim_seq u -> ex_lim_seq (fun n => a * u n).
proof: Proof. move => [l H]. exists (Rbar_mult a l). eapply is_lim_seq_scal_l ; try eassumption. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy