use 0
case h.inl
n : ℕ
ih :
  ∀ m < n,
    ∀ {a : ℤ√(-3)},
      IsCoprime a.re a.im →
        a.norm.natAbs = m →
          ∃ 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
hn : a.norm.natAbs = n
h : a.norm = 1
⊢ ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
case h
n : ℕ
ih :
  ∀ m < n,
    ∀ {a : ℤ√(-3)},
      IsCoprime a.re a.im →
        a.norm.natAbs = m →
          ∃ 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
hn : a.norm.natAbs = n
h : a.norm = 1
⊢ (a = Multiset.prod 0 ∨ a = -Multiset.prod 0) ∧ ∀ pq ∈ 0, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs