lean_workbook_plus_38763
ProvedIf , prove that \n\n .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_38763 (a : ℝ) (h : a > 0) : 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_38763 (a : ℝ) (h : a > 0) : 1 / Real.sqrt a > 2 * (Real.sqrt (a + 1) - Real.sqrt a) := by sorry