intro h
p : ℤ√(-3)
hfour : p.norm = 4
hq : p.im ≠ 0
this : p.re ^ 2 = 1 ∧ p.im ^ 2 = 1
⊢ p.im ^ 2 = 1 → |p.im| = 1
p : ℤ√(-3)
hfour : p.norm = 4
hq : p.im ≠ 0
this : p.re ^ 2 = 1 ∧ p.im ^ 2 = 1
h : p.im ^ 2 = 1
⊢ |p.im| = 1