constructor <;> ring
case intro.inl.intro.h
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 = 4 * v - a.im
⊢ 4 * v - a.im = 1 * (v - a.im) + -3 * -1 * v ∧ a.im = 1 * v + -1 * (v - a.im)
no goals