refine' mul_le_mul_of_nonneg_left (upper_monotone_aux _) (by positivity)
n : ℕ
⊢ 4 * ((↑n + 1 / 2) / (↑n + 1)) ≤ 4 * (Real.sqrt (↑n + 1 / 3) / Real.sqrt (↑n + 1 + 1 / 3))

case b0
n : ℕ
⊢ 0 < ↑(centralBinom n)

case d0
n : ℕ
⊢ 0 < Real.sqrt (↑(n + 1) + 1 / 3)

n : ℕ
⊢ 0 < 4
case b0
n : ℕ
⊢ 0 < ↑(centralBinom n)

case d0
n : ℕ
⊢ 0 < Real.sqrt (↑(n + 1) + 1 / 3)

n : ℕ
⊢ 0 < 4