proposition: Lemma pseries_diffs_sumE n f x : \sum_(0 <= i < n) pseries_diffs f i * x ^+ i = (\sum_(0 <= i < n) i%:R * f i * x ^+ i.-1) + n%:R * f n * x ^+ n.-1.
proof: Proof. case: n => [|n]; first by rewrite !big_nil !mul0r add0r. under eq_bigr do unfold pseries_diffs. by rewrite big_nat_recr //= big_nat_recl //= !mul0r add0r. 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