lean_workbook_plus_19568
ProvedIf , prove that \n\n .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_19568 (a : ℝ) (ha : 0 < a) : 1 / Real.sqrt a > 2 * (Real.sqrt (a + 1) - Real.sqrt a) := by sorry
Source
If , prove that \n\n .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_19568 (a : ℝ) (ha : 0 < a) : 1 / Real.sqrt a > 2 * (Real.sqrt (a + 1) - Real.sqrt a) := by sorry