proposition: Lemma is_cvg_pseries_diffs_equiv f x : cvgn (pseries (pseries_diffs f) x) -> cvgn ([series i%:R * f i * x ^+ i.-1]_i).
proof: Proof. by by move=> Cx; have := pseries_diffs_equiv Cx; move/(cvg_lim _) => -> //. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(boolp classical_sets functions) mathcomp(mathcomp_extra) reals ereal signed topology normedtype landau sequences derive realfun itv convex