contrapose! hp
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hp : ¬IsUnit p
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
⊢ ¬(p ∈ s ∧ star p ∈ s)
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
hp : p ∈ s ∧ star p ∈ s
⊢ IsUnit p