Theorem: C03S05.MyAbs.neg_le_abs_self (LeanInRome/S3_Logic/S05_Disjunction.lean)

State before:
x✝ y x : ℝ
⊢ -x ≤ |x|
Tactic:
sorry
State after:
no goals