have hterm : ∀ i : ℕ, i ∈ Finset.range n → 1 ≤ x^i * y^(n - 1 - i) := by
  intro i _
  calc 1 ≤ x^i             := one_le_pow_of_one_le hx.le i
       _ = x^i * 1         := (mul_one _).symm
       _ ≤ x^i * y^(n-1-i) := by gcongr; apply one_le_pow_of_one_le hy.le
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 : ℕ
⊢ (x - y) * ↑n ≤ x ^ n - 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