Theorem: sq_add_sq_ne_zero (PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hy : y ≠ 0
⊢ x ^ 2 + y ^ 2 ≠ 0
Tactic:
linarith [sq_nonneg x, sq_pos_iff.mpr hy]
State after:
no goals