apply Multiset.prod_nonneg
case ha
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ 0 ≤ Multiset.prod (factorsOddPrimeOrFour a)
case ha.h
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ ∀ (a_1 : ℤ), a_1 ∈ factorsOddPrimeOrFour a → 0 ≤ a_1