simp only [abs_neg, abs_lt]
case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.refl

⊢ |21| < 24
case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.refl

⊢ -24 < 21 ∧ 21 < 24