. apply pow_nonneg (by norm_num)
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 b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))