Sum of geometric series (finite)

import Mathlib

theorem geom_sum_finite {R : Type*} [CommRing R] (x : R) (n : ℕ) (h : x ≠ 1) : (∑ i ∈ Finset.range n, x ^ i) * (x - 1) = x ^ n - 1 := by
  have _ := h
  exact geom_sum_mul x n