proposition: Lemma Lim_seq_scal_r (u : nat -> R) (a : R) : Lim_seq (fun n => u n * a) = Rbar_mult (Lim_seq u) a.
proof: Proof. rewrite Rbar_mult_comm -Lim_seq_scal_l. apply Lim_seq_ext ; by intuition. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy