no goals
α : Type u
inst✝ : Ring α
x : α
m n : ℕ
hmn : m ≤ n
⊢ (∑ i in Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n
rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul_neg, geom_sum_mul_neg, sub_sub_sub_cancel_left]