proposition: Lemma geometric_le_lim {R : realType} (n : nat) (a x : R) : 0 <= a -> 0 < x -> `|x| < 1 -> series (geometric a x) n <= a * (1 - x)^-1.
proof: Proof. move=> a0 x0 x1. have /(@cvg_unique _ (@Rhausdorff R)) := @cvg_geometric_series _ a _ x1. move/(_ _ (@is_cvg_geometric_series _ a _ x1)) => ->. apply: nondecreasing_cvgn_le; last exact: is_cvg_geometric_series. by apply: nondecreasing_series => ? _ /=; rewrite pmulr_lge0 // exprn_gt0. 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