cases' h0 with h0 h0 <;> [(use -1), (use 1)] <;> convert h0 using 1 <;>
  simp only [Units.val_neg, Units.val_one, neg_mul, one_mul]
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
⊢ ∃ A, Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
case h.e'_4
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im
⊢ p.re * a.im + -(a.re * p.im) = p.re * a.im - a.re * p.im