rw [Int.natAbs_pow] at hp
case inr.intro
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
hp : (p.re ^ 2).natAbs.Prime
⊢ False
case inr.intro
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
hp : (p.re.natAbs ^ 2).Prime
⊢ False