lean_workbook_plus_42647

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

If $x<0$ , then $|x|=-x$ ; if also $x+k<0$ , then we get $|x+k|=-x-k\ne -x+k$ since $k\ne0$ ; if instead $x+k\ge0$ , then $|x+k|=x+k\ne -x+k$ since $x\ne0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_42647  (x k : ℝ)
  (h₀ : x < 0)
  (h₁ : x + k < 0)
  (h₂ : k ≠ 0) :
  |x + k| ≠ -x + k   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph