proposition: Lemma is_pseries_incr_1 (a : nat -> V) (x:K) (l : V) : is_pseries a x l -> is_pseries (PS_incr_1 a) x (scal x l).
proof: Proof. move => Ha. apply filterlim_ext_loc with (fun n : nat => scal x (sum_n (fun k => scal (pow_n x k) (a k)) (pred n))). exists 1%nat; intros n; case n. intros Hn; contradict Hn ; apply Nat.nlt_0_r. clear n; intros n _ ;induction n. now rewrite /= !sum_Sn !sum_O /= mult_one_r 2!scal_one plus_zero_l. apply trans_eq with (plus (sum_n (fun k : nat => scal (pow_n x k) (PS_incr_1 a k)) (S n)) (scal (pow_n x (S (S n))) (PS_incr_1 a (S (S n))))). 2: rewrite /= !sum_Sn ; reflexivity. rewrite -IHn; simpl. rewrite !sum_Sn scal_distr_l; apply f_equal. now rewrite scal_assoc. apply filterlim_comp with (f:= fun n => pred n) (G:=eventually) (g:=fun n => scal x (sum_n (fun k : nat => scal (pow_n x k) (a k)) n)). apply eventually_subseq_loc. exists 1%nat. intros n Hn. rewrite -pred_Sn. now apply Nat.lt_pred_l, Nat.neq_0_lt_0. 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