have : star p ≠ p := by
  rw [Ne, Zsqrtd.ext_iff]
  rintro ⟨-, H⟩
  apply him
  apply eq_zero_of_neg_eq
  simpa using H
case neg
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime s.prod.re s.prod.im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
⊢ IsUnit p
case neg
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime s.prod.re s.prod.im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
this : star p ≠ p
⊢ IsUnit p