apply Int.eq_of_associated_of_nonneg
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ Multiset.prod (factorsOddPrimeOrFour a) = a
case h
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) a

case ha
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ 0 ≤ Multiset.prod (factorsOddPrimeOrFour a)

case hb
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ 0 ≤ a