proposition: Lemma is_series_scal (c : K) (a : nat -> V) (l : V) : is_series a l -> is_series (fun n => scal c (a n)) (scal c l).
proof: Proof. move => Ha. apply filterlim_ext with (fun n => scal c (sum_n a n)). elim => [ | n IH]; simpl. by rewrite !sum_O. rewrite !sum_Sn -IH. apply: scal_distr_l. now apply filterlim_comp with (2 := filterlim_scal_r _ _). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy