Negative binomial positive tail tsum

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Normed.Ring.Basic
import Mathlib.Analysis.SpecificLimits.Normed
import Mathlib.Data.Sym.Basic
import Mathlib.Data.Sym.Card
import Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

section
open Finset

namespace D1Bound5


theorem _root_.D1Bound5.negative_binomial_positive_tail_tsum (q : ℕ) (r : ℝ)
    (hr0 : 0 ≤ r) (hr1 : r < 1) :
    (∑' j : ℕ, (Nat.choose (j + 1 + q) q : ℝ) * r ^ (j + 1)) =
      1 / (1 - r) ^ (q + 1) - 1 := by sorry



end D1Bound5
end