rw [eq_comm]
case h.e'_2
x : ℕ
hx : ¬x = 0
a : ℕ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
⊢ 2 = a ∨ Odd a
case h.e'_2
x : ℕ
hx : ¬x = 0
a : ℕ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
⊢ a = 2 ∨ Odd a