Update Reductions.lean

Co-Authored-By: Yaël Dillies <[email protected]>

FLT/Basic/Reductions.lean

@@ -254,15 +254,10 @@ lemma FreyCurve.j (P : FreyPackage) :
   rw [mul_div_right_comm, EllipticCurve.j, FreyCurve.Δ'inv, FreyCurve.c₄']
 
 private lemma j_pos_aux (a b : ℤ) (hb : b ≠ 0) : 0 < (a + b) ^ 2 - a * b := by
-  cases le_or_lt 0 (a * b) with
-  | inl h =>
-    rify
-    calc
+  rify
+  calc
       (0 : ℝ) < (a ^ 2 + (a + b) ^ 2 + b ^ 2) / 2 := by positivity
       _ = (a + b) ^ 2 - a * b := by ring
-  | inr h =>
-    rw [sub_pos]
-    exact h.trans_le (sq_nonneg _)
 
 /-- The q-adic valuation of the j-invariant of the Frey curve is a multiple of p if 2 < q is
 a prime of bad reduction. -/