From 2b56232019955ac6af6b935382c277cb6d2098f2 Mon Sep 17 00:00:00 2001 From: Heath Sanchez Date: Mon, 6 Jul 2026 15:11:58 +1200 Subject: [PATCH] Fill two local arithmetic steps in Chapter 03 --- FormalBook/Chapter_03.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/FormalBook/Chapter_03.lean b/FormalBook/Chapter_03.lean index fa35bc1..19f1266 100644 --- a/FormalBook/Chapter_03.lean +++ b/FormalBook/Chapter_03.lean @@ -150,7 +150,7 @@ theorem binomials_coefficients_never_powers (k l m n : ℕ) (h_2lel : 2 ≤ l) ( -- STEP (4) : l ≥ 3 by Contradiction -- case l ≥ 3 · have h_3lel : 3 ≤ l := by - sorry + omega -- main work : n < k³ have h₄ : n < k^3 := by sorry @@ -170,7 +170,7 @@ theorem binomials_coefficients_never_powers (k l m n : ℕ) (h_2lel : 2 ≤ l) ( have h_k'_def : k' = n - k := by rfl -- third requirement: 2 * k' ≤ n have h_2k'len : 2 * k' ≤ n := by - sorry + omega -- second requirement: k ≤ n - 4 have h_k'len4 : k' ≤ n - 4 := by simp only [h_k'_def, tsub_le_iff_right]