use French

riccardobrasca · Jan 22, 2025 · ac3d9de · ac3d9de
1 parent 077a697
commit ac3d9de
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Math2001/01_Proofs_by_Calculation/04_Proving_Inequalities.lean b/Math2001/01_Proofs_by_Calculation/04_Proving_Inequalities.lean
@@ -27,7 +27,7 @@ example {r s : ℚ} (h1 : s + 3 ≥ r) (h2 : s + r ≤ 3) : r ≤ 3 := by
   done
 
 -- Example 1.4.3
--- Exercise: type out the whole proof printed in the text as a Lean proof.
+-- Exercice : écrire l'ensemble de la preuve dans comme une preuve en Lean.
 example {x y : ℝ} (h1 : y ≤ x + 5) (h2 : x ≤ -2) : x + y < 2 := by
   sorry
   done