proposition: Lemma cvg_geometric_series (R : archiFieldType) (a z : R) : `|z| < 1 -> series (geometric a z) @ \oo --> (a * (1 - z)^-1).
proof: Proof. move=> Nz_lt1; rewrite geometric_seriesE ?lt_eqF 1?ltr_normlW//. have -> : a / (1 - z) = (a * (1 - 0)) / (1 - z) by rewrite subr0 mulr1. by apply: cvgMl; apply: cvgMr; apply: cvgB; [apply: cvg_cst|apply: cvg_expr]. 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