proposition: Lemma PSeries_decr_n (a : nat -> R) (n : nat) (x : R) : ex_pseries a x -> PSeries a x = sum_f_R0 (fun k => a k * x^k) n + x^(S n) * PSeries (PS_decr_n a (S n)) x.
proof: Proof. intros Ha. case: (Req_dec x 0) => Hx. rewrite Hx PSeries_0 ; simpl ; ring_simplify. elim: n => /= [ | n IH]. ring. rewrite -IH ; ring. assert (V:(pow_n x (S n) <> 0)). rewrite pow_n_pow; now apply pow_nonzero. move: (is_pseries_decr_n a (S n) x (/x) (PSeries a x) (Rinv_l x Hx) (Nat.lt_0_succ _) (PSeries_correct _ _ Ha)) => Hb. rewrite (is_pseries_unique _ _ _ Hb). rewrite (sum_n_ext _ (fun k : nat => a k * x ^ k)). rewrite sum_n_Reals. replace (S n -1)%nat with n. rewrite /scal /plus /opp /= /mult /=. rewrite pow_n_pow -Rinv_pow ; try assumption. field. split; try assumption. now apply pow_nonzero. now rewrite Nat.sub_succ Nat.sub_0_r. intros m; rewrite pow_n_pow. apply Rmult_comm. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series