suffices
  ∀ n : ℕ,
    a.norm.natAbs = n →
      ∃ f : Multiset (ℤ√(-3)),
        (a = f.prod ∨ a = -f.prod) ∧
          ∀ pq : ℤ√(-3), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
  by exact this a.norm.natAbs rfl
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ ∀ (n : ℕ),
    a.norm.natAbs = n →
      ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs