proposition: Lemma PSeries_incr_1 a x : PSeries (PS_incr_1 a) x = x * PSeries a x.
proof: Proof. rewrite -Series_scal_l. unfold PSeries, Series. rewrite -(Lim_seq_incr_1 (sum_n (fun k : nat => PS_incr_1 a k * x ^ k))) /=. apply f_equal, Lim_seq_ext. case. rewrite sum_Sn !sum_O /= /plus /zero /=. ring. elim => /= [ | n IH]. rewrite !sum_Sn !sum_O /= /plus /zero /=. ring. rewrite sum_Sn IH !sum_Sn /= /plus /=. ring. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series