proposition: Lemma geometric_seriesE (R : numFieldType) (a z : R) : z != 1 -> series (geometric a z) = [sequence a * (1 - z ^+ n) / (1 - z)]_n.
proof: Proof. rewrite funeqE => z_neq1 n. apply: (@mulIf _ (1 - z)); rewrite ?mulfVK ?subr_eq0 1?eq_sym//. rewrite seriesEnat !mulrBr [in LHS]mulr1 mulr_suml -opprB -sumrB. by under eq_bigr do rewrite -mulrA -exprSr; rewrite telescope_sumr// opprB. 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