simp [h2]
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)
no goals