proposition: Lemma PSeries_incr_n (a : nat -> R) (n : nat) (x : R) : PSeries (PS_incr_n a n) x = x^n * PSeries a x.
proof: Proof. elim: n => /= [ | n IH]. by rewrite Rmult_1_l. rewrite Rmult_assoc. by rewrite PSeries_incr_1 IH. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series