rw [sub_eq_iff_eq_add] at hv
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v + a.im, im := v }
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v + a.im, im := v }