lean_workbook_plus_70226
ProvedProve for .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70226 (s : ℝ) (hs : s ≥ 3) : (3 * s) / (2 * s + 3) ≤ s / Real.sqrt (s + 6) := by sorry
Source
Prove for .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_70226 (s : ℝ) (hs : s ≥ 3) : (3 * s) / (2 * s + 3) ≤ s / Real.sqrt (s + 6) := by sorry