proposition: Lemma cvg_expr (R : archiFieldType) (z : R) : `|z| < 1 -> (GRing.exp z : R ^nat) @ \oo --> (0 : R).
proof: Proof. move=> Nz_lt1; apply/norm_cvg0P; pose t := (1 - `|z|). apply: (@squeeze_cvgr _ _ _ _ (cst 0) (t^-1 *: @harmonic R)); last 2 first. - exact: cvg_cst. - by rewrite -(scaler0 _ t^-1); exact: (cvgZr cvg_harmonic). near=> n; rewrite normr_ge0 normrX/= ler_pdivlMl ?subr_gt0//. rewrite -(@ler_pM2l _ n.+1%:R)// mulfV// [t * _]mulrC mulr_natl. have -> : 1 = (`|z| + t) ^+ n.+1 by rewrite addrC addrNK expr1n. rewrite exprDn (bigD1 (inord 1)) ?inordK// subn1 expr1 bin1 lerDl sumr_ge0//. by move=> i; rewrite ?(mulrn_wge0, mulr_ge0, exprn_ge0, subr_ge0)// ltW. Unshelve. all: by end_near. 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