calc (x - y) * (n : ℝ)
    = (n : ℝ) * (x - y) := mul_comm _ _
  _ = (∑ _i in Finset.range n, (1 : ℝ)) * (x - y) :=
                             by simp only [mul_one, Finset.sum_const, nsmul_eq_mul,
                                Finset.card_range]
  _ ≤ (∑ i in Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x-y) :=
                              (mul_le_mul_right hxmy).mpr (Finset.sum_le_sum hterm)
  _ = x^n - y^n         := geom_sum₂_mul x y n
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)
⊢ (x - y) * ↑n ≤ x ^ n - y ^ n
no goals