suffices H : abs a.re = 1
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
⊢ abs a.re = 1 ∧ a.im = 0
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
H : abs a.re = 1
⊢ abs a.re = 1 ∧ a.im = 0

case H
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
⊢ abs a.re = 1