rw [hassoc, Int.natAbs_pos]
case refine_1
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ 0 < f.prod
case refine_1
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ a.norm ≠ 0