obtain rfl | rfl := hu
case intro
a p : ℤ√(-3)
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a
hpprime : Prime (Zsqrtd.norm p)
u : ℤ√(-3)
hu : a = p * u ∨ a = star p * u
⊢ Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u
case intro.inl
p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
u : ℤ√(-3)
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm (p * u)
⊢ Zsqrtd.norm (p * u) = Zsqrtd.norm p * Zsqrtd.norm u

case intro.inr
p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
u : ℤ√(-3)
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm (star p * u)
⊢ Zsqrtd.norm (star p * u) = Zsqrtd.norm p * Zsqrtd.norm u