proposition: Lemma is_series_scal_l : forall (c : K) (a : nat -> V) (l : V), is_series a l -> is_series (fun n => scal c (a n)) (scal c l).
proof: Proof. exact is_series_scal. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy