no goals
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ ∑ i in Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)
simp only [sum_Ico_eq_sub _ hmn, geom_sum_eq hx, div_sub_div_same, sub_sub_sub_cancel_right]