cases ha with
| inl ha =>
  rw [Multiset.eq_of_mem_replicate ha]
  norm_num
| inr ha =>
  exact oddFactors.nonneg ha
z a : ℤ
ha : a ∈ Multiset.replicate (evenFactorExp z / 2) 4 ∨ a ∈ oddFactors z
⊢ 0 ≤ a
no goals