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

State before:
x y : ℝ
⊢ |x| < y ↔ -y < x ∧ x < y
Tactic:
sorry
State after:
no goals