rw [hc]
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : |x| = c.norm
⊢ ∃ c, |x| = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : |x| = c.norm
⊢ ∃ c_1, c.norm = c_1.norm ∧ 0 ≤ c_1.re ∧ c_1.im ≠ 0