proposition: Lemma PSeries_decr_1_aux (a : nat -> R) (x : R) : a O = 0 -> (PSeries a x) = x * PSeries (PS_decr_1 a) x.
proof: Proof. intros Ha0. rewrite -PSeries_incr_1. rewrite /PS_incr_1 /PS_decr_1 /=. apply Series_ext. case => //=. by rewrite Ha0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series