have heq : x.norm = y.norm :=
  haveI hd : (-3 : ℤ) ≤ 0 := by norm_num
  Int.eq_of_associated_of_nonneg h (Zsqrtd.norm_nonneg hd _) (Zsqrtd.norm_nonneg hd _)
x y : ℤ√(-3)
h : Associated x.norm y.norm
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour x.norm.natAbs
⊢ Associated' x y
x y : ℤ√(-3)
h : Associated x.norm y.norm
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour x.norm.natAbs
heq : x.norm = y.norm
⊢ Associated' x y