proposition: Lemma PSeries_decr_1 (a : nat -> R) (x : R) : ex_pseries a x -> PSeries a x = a O + x * PSeries (PS_decr_1 a) x.
proof: Proof. intros Ha. case: (Req_dec x 0) => Hx. rewrite Hx PSeries_0 ; ring. move: (is_pseries_decr_1 a x (/x) (PSeries a x) (Rinv_l _ Hx) (PSeries_correct _ _ Ha)) => Hb. rewrite (is_pseries_unique _ _ _ Hb). rewrite /plus /opp /scal /= /mult /=. now field. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series