proposition: Lemma eseriesSB (n : nat) : eseries n \is a fin_num -> eseries n.+1 - eseries n = u_ n.
proof: Proof. by move=> enfin; rewrite eseriesS addeK//=. 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