have hNp : 0 < N := by exact_mod_cast (one_div_pos.mpr hxmy).trans hN
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
⊢ 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
⊢ False