obtain ⟨v, hv⟩ := hdvd
case intro.inr
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
ha : Odd a.re
hb : Odd a.im
hdvd : 4 ∣ a.re - a.im
⊢ ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u
case intro.inr.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u