proposition: Lemma ex_pseries_incr_n (a : nat -> V) (n : nat) (x : K) : ex_pseries a x -> ex_pseries (PS_incr_n a n) x.
proof: Proof. move => [l Ha]. exists (scal (pow_n x n) l) ; by apply is_pseries_incr_n. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series