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 (Zsqrtd.norm x) (Zsqrtd.norm y)
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour (Zsqrtd.norm x)
⊢ Associated' x y
x y : ℤ√(-3)
h : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour (Zsqrtd.norm x)
heq : Zsqrtd.norm x = Zsqrtd.norm y
⊢ Associated' x y