harder

riccardobrasca · Jan 22, 2025 · 4746882 · 4746882
1 parent ac3d9de
commit 4746882
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Math2001/01_Proofs_by_Calculation/05_A_Shortcut.lean b/Math2001/01_Proofs_by_Calculation/05_A_Shortcut.lean
@@ -19,7 +19,7 @@ example {x y : ℚ} (hx : x = 2) (hy : y ^ 2 = -7) : x + y ^ 2 = -5 := by
   done
 
 example {s t : ℝ} (h : t = 4 - s * t) : t + s * t > 0 := by
-  addarith [h]
+  sorry
   done
 
 example {m n : ℝ} (h1 : m ≤ 8 - n) : 10 > m + n := by