proposition: Lemma is_pseries_scal (c : K) (a : nat -> V) (x : K) (l : V) : mult x c = mult c x -> is_pseries a x l -> is_pseries (PS_scal c a) x (scal c l).
proof: Proof. move => Hx Ha. apply (filterlim_ext (fun n => scal c (sum_n (fun k => scal (pow_n x k) (a k)) n))). elim => [ | n IH]. simpl ; rewrite /PS_scal. rewrite !sum_O. now repeat rewrite scal_one. simpl ; rewrite !sum_Sn -IH /PS_scal. rewrite scal_distr_l; apply f_equal. rewrite 2! scal_assoc. apply f_equal2. rewrite -/(pow_n x (S n)). clear -Hx. elim: (S n) => {n} /= [ | n IH]. by rewrite mult_one_l mult_one_r. by rewrite -mult_assoc -IH 2!mult_assoc Hx. by []. now apply filterlim_comp with (2 := filterlim_scal_r _ _). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series