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

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