rw [← Zsqrt3.norm_natAbs]
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hq : p.im ≠ 0
hp : p.norm.natAbs = 4
⊢ p.norm = 4
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hq : p.im ≠ 0
hp : p.norm.natAbs = 4
⊢ ↑p.norm.natAbs = 4