Solving an affine strict inequality
ProvedWorkbookSource.problem_3002lean-workbooksource-checked
Solve the inequality. $x+1\dfrac{1}{2}>0$
Source: InternLM Lean-Workbook, record lean_workbook_3002 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.problem_3002 (x : ℝ) : x + 1.5 > 0 ↔ x > -1.5 := by sorry
Source