simp only [mul_one, Finset.sum_const, nsmul_eq_mul,
Finset.card_range]
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n : ℕ
hterm : ∀ i ∈ Finset.range n, 1 ≤ x ^ i * y ^ (n - 1 - i)
⊢ ↑n * (x - y) = (∑ _i ∈ Finset.range n, 1) * (x - y)
no goals