rcases Nat.Prime.eq_two_or_odd' hprime with (h2 | hodd)
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Nat.Prime (Int.natAbs a)
this : ↑(Int.natAbs a) = a
⊢ 2 = ↑(Int.natAbs a) ∨ Odd ↑(Int.natAbs a)
case h.e'_2.inl
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Nat.Prime (Int.natAbs a)
this : ↑(Int.natAbs a) = a
h2 : Int.natAbs a = 2
⊢ 2 = ↑(Int.natAbs a) ∨ Odd ↑(Int.natAbs a)

case h.e'_2.inr
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Nat.Prime (Int.natAbs a)
this : ↑(Int.natAbs a) = a
hodd : Odd (Int.natAbs a)
⊢ 2 = ↑(Int.natAbs a) ∨ Odd ↑(Int.natAbs a)