rw [← Int.abs_eq_normalize, ← Int.coe_natAbs] at this
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Prime a
this : ↑normalize a = a
⊢ 2 = a ∨ Odd a
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Prime a
this : ↑(Int.natAbs a) = a
⊢ 2 = a ∨ Odd a