theorem C03S05.MyAbs.le_abs_self (x : ℝ) : x ≤ |x|

theorem C03S05.MyAbs.neg_le_abs_self (x : ℝ) : -x ≤ |x|

theorem C03S05.MyAbs.abs_add (x : ℝ) (y : ℝ) : |x + y| ≤ |x| + |y|

theorem C03S05.MyAbs.lt_abs {x : ℝ} {y : ℝ} : x < |y| ↔ x < y ∨ x < -y

theorem C03S05.MyAbs.abs_lt {x : ℝ} {y : ℝ} : |x| < y ↔ -y < x ∧ x < y