[Iran1998Q9] simplify after field_simp improvement leanprover-communi…

…ty/mathlib4@6b391ef
dwrensha · Aug 27, 2023 · b270396 · b270396
1 parent 229a670
commit b270396
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/MathPuzzles/Iran1998Q9.lean b/MathPuzzles/Iran1998Q9.lean
@@ -46,10 +46,6 @@ theorem iran1998_q9
   --
   -- The desired result follows.
 
-  have hxz : x ≠ 0 := by positivity
-  have hyz : y ≠ 0 := by positivity
-  have hzz : z ≠ 0 := by positivity
-
   have hx0 : 0 ≤ x := by positivity
   have hy0 : 0 ≤ y := by positivity
   have hz0 : 0 ≤ z := by positivity