nat abs or

Stream: Is there code for X?

[Bolton Bailey]

Do we have something like this?
lemma nat_abs_or (z : ℤ) : (z.nat_abs : ℤ) = z ∨ (z.nat_abs : ℤ) = (-z)

[Bhavik Mehta]

I think int.nat_abs_eq_iff.1 rfl essentially gives you this (docs#int.nat_abs_eq_iff)