use ⟨v + a.im, v⟩
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ ∃ b, a.norm = 4 * b.norm
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ a.norm = 4 * { re := v + a.im, im := v }.norm