case h.e'_3
α : Type ?u.578354
β : Type ?u.578357
n d k N : ℕ
x : Fin n → ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ^ (↑n - 2) / ↑n = ↑d ^ ↑n / ↑(n * d ^ 2)
α : Type ?u.578354
β : Type ?u.578357
n d k N : ℕ
x : Fin n → ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ^ (↑n - 2) / ↑n ≤ ↑(↑rothNumberNat ((2 * d - 1) ^ n))
convert bound_aux' n d using 1
no goals
case h.e'_3
α : Type ?u.578354
β : Type ?u.578357
n d k N : ℕ
x : Fin n → ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ^ (↑n - 2) / ↑n = ↑d ^ ↑n / ↑(n * d ^ 2)
rw [cast_mul, cast_pow, mul_comm, ← div_div, ← cast_two, ← cast_sub hn, rpow_nat_cast,
  rpow_nat_cast, pow_sub₀ _ (cast_ne_zero.2 hd) hn, ← div_eq_mul_inv]