. rw [← Real.rpow_nat_cast]
  rw [Real.rpow_le_rpow_left_iff (by norm_cast)]
  rw [le_div_iff (by norm_num)]
  norm_cast
  apply Nat.le_trans (Nat.mul_le_mul_right 3 (Nat.pred_le _))
  apply Nat.div_mul_le_self
case h₂
n : ℕ
hn : 0 < n
⊢ 4 ^ Nat.pred (2 * n / 3) ≤ 4 ^ (2 * ↑n / 3)

case c0
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4 ^ Nat.pred (2 * n / 3)

case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
case c0
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4 ^ Nat.pred (2 * n / 3)

case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))