have h1 := calc 1 = (x - y) * (1 / (x - y)) := by field_simp
             _ < (x - y) * N             := (mul_lt_mul_left hxmy).mpr hN
             _ ≤ x^N - y^N               := hn N
case intro
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
N : ℕ
hN : 1 / (x - y) < ↑N
hNp : 0 < N
⊢ False
case intro
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
N : ℕ
hN : 1 / (x - y) < ↑N
hNp : 0 < N
h1 : 1 < x ^ N - y ^ N
⊢ False