lean_workbook_plus_61117
ProvedProve that for .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61117 (a : ℝ) (h : a ≤ 2) : Real.sqrt ((a - 2) ^ 2) = 2 - a := by sorry
Source
Prove that for .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_61117 (a : ℝ) (h : a ≤ 2) : Real.sqrt ((a - 2) ^ 2) = 2 - a := by sorry