apply le_antisymm
p : ℤ√(-3)
hfour : p.norm = 4
hq : p.im ≠ 0
⊢ p.im ^ 2 = 1
case a
p : ℤ√(-3)
hfour : p.norm = 4
hq : p.im ≠ 0
⊢ p.im ^ 2 ≤ 1

case a
p : ℤ√(-3)
hfour : p.norm = 4
hq : p.im ≠ 0
⊢ 1 ≤ p.im ^ 2