proposition: Lemma ex_pseries_decr_1 (a : nat -> V) (x : K) : (x = zero \/ exists y, mult y x = one) -> ex_pseries a x -> ex_pseries (PS_decr_1 a) x.
proof: Proof. case => [H | [y Hx]] [l Ha]. rewrite H ; by apply ex_pseries_0. exists (scal y (plus l (opp (a 0%nat)))). now apply is_pseries_decr_1. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series