obtain rfl | ⟨hprime, hodd⟩ := hx
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hx : OddPrimeOrFour x
hfactor : x ∣ Zsqrtd.norm a
⊢ ∃ c, Abs.abs x = Zsqrtd.norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0
case inl
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hfactor : 4 ∣ Zsqrtd.norm a
⊢ ∃ c, Abs.abs 4 = Zsqrtd.norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0

case inr.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
⊢ ∃ c, Abs.abs x = Zsqrtd.norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0