{K : Type u_4} →
  [inst : NormedRing K] →
    {motive : HasSummableGeomSeries K → Sort u} →
      ((summable_geometric_of_norm_lt_one : ∀ (ξ : K), ‖ξ‖ < 1 → Summable fun n => ξ ^ n) → motive ⋯) →
        (t : HasSummableGeomSeries K) → motive t