have hn : ∀ n : ℕ, (x - y) * (n : ℝ) ≤ x^n - y^n := fun n ↦ by
  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
  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
⊢ False
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
⊢ False