neg_eq_zero for complex numbers?

Stream: new members

[Răzvan Flavius Panda]

z_rez_im: ℝ
h: ¬{re := z_re, im := z_im} = 0
⊢ 0 < z_re ^ 2 + z_im ^ 2

I'm stuck on this goal and not sure how to make progress since neg_eq_zero is not working

[Kevin Buzzard]

Do you know the maths proof?

[Kevin Buzzard]

neg_eq_zero says $-x=0\implies x=0$. I'm not sure what it has to do with this.

[Kevin Buzzard]

$-$ is negative, not logical "not".

[Kevin Buzzard]

[discussion moved elsewhere]