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