proposition: Lemma ex_pseries_decr_n (a : nat -> V) (n : nat) (x : K) : (x = zero \/ exists y, mult y x = one) -> ex_pseries a x -> ex_pseries (PS_decr_n a n) x.
proof: Proof. intros Hx H. induction n. unfold PS_decr_n; now simpl. apply ex_pseries_ext with ((PS_decr_1 (PS_decr_n a n))). intros m; unfold PS_decr_1, PS_decr_n. apply f_equal; ring. apply ex_pseries_decr_1. apply Hx. now apply IHn. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series