proposition: Lemma PSeries_decr_n_aux (a : nat -> R) (n : nat) (x : R) : (forall k : nat, (k < n)%nat -> a k = 0) -> PSeries a x = x^n * PSeries (PS_decr_n a n) x.
proof: Proof. elim: n => /= [ | n IH] Ha. rewrite Rmult_1_l. apply PSeries_ext => n ; by intuition. rewrite IH. rewrite PSeries_decr_1_aux. rewrite (Rmult_comm _ (x^n)) Rmult_assoc. repeat apply Rmult_eq_compat_l. apply PSeries_ext => k ; rewrite /PS_decr_1 /PS_decr_n ; by intuition. apply Ha ; by intuition. move => k Hk. apply Ha ; by intuition. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series