proposition: Lemma is_pseries_incr_n (a : nat -> V) (n : nat) (x : K) (l : V) : is_pseries a x l -> is_pseries (PS_incr_n a n) x (scal (pow_n x n) l).
proof: Proof. move => Ha. elim: n => /= [ | n IH]. by rewrite scal_one. rewrite -scal_assoc. by apply is_pseries_incr_1. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series