have hdvd : p'.norm ∣ p.norm := by rw [heq]
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour p.norm.natAbs
heq : p.norm = p'.norm
⊢ |p.re| = |p'.re| ∧ |p.im| = |p'.im|
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour p.norm.natAbs
heq : p.norm = p'.norm
hdvd : p'.norm ∣ p.norm
⊢ |p.re| = |p'.re| ∧ |p.im| = |p'.im|