proposition: Lemma telescopeK (V : zmodType) (u_ : V ^nat) : series (telescope u_) = [sequence u_ n - u_ 0%N]_n.
proof: Proof. by rewrite funeqE => n; rewrite seriesEnat/= telescope_sumr. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau