rintro a ha ⟨rfl, hodd⟩
case h.e'_3.h.e'_6
x : ℕ
hx : ¬x = 0
⊢ ∀ a ∈ UniqueFactorizationMonoid.normalizedFactors x, ¬(2 = a ∧ Odd a)
case h.e'_3.h.e'_6.intro
x : ℕ
hx : ¬x = 0
ha : 2 ∈ UniqueFactorizationMonoid.normalizedFactors x
hodd : Odd 2
⊢ False