rw [le_div_iff, mul_assoc, mul_comm, ← div_le_div_iff, centralBinom_ratio, mul_comm,
  mul_div_assoc, Nat.cast_add_one]
n : ℕ
⊢ ↑(centralBinom n) * Real.sqrt (↑n + 1 / 4) ≤ ↑(centralBinom (n + 1)) * Real.sqrt (↑(n + 1) + 1 / 4) / 4
n : ℕ
⊢ 4 * (Real.sqrt (↑n + 1 / 4) / Real.sqrt (↑n + 1 + 1 / 4)) ≤ 4 * ((↑n + 1 / 2) / (↑n + 1))

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

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

n : ℕ
⊢ 0 < 4