use star q'
case h.inr
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : q'.norm ∣ a.norm
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvdvd : a.norm = q'.norm * u.norm
huv : a = star q' * u
⊢ ∃ q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
case h
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : q'.norm ∣ a.norm
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvdvd : a.norm = q'.norm * u.norm
huv : a = star q' * u
⊢ 0 ≤ (star q').re ∧
    (star q').im ≠ 0 ∧ OddPrimeOrFour (star q').norm.natAbs ∧ a = star q' * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm