From c0fc5a58510b5fd74a7132d9ae11a4517cffb8c6 Mon Sep 17 00:00:00 2001 From: Florian Grandel Date: Sun, 7 Jun 2026 21:53:43 +0200 Subject: [PATCH] C02_Basics: solutions: streamlined example --- MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean b/MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean index 0502aafd..b1efeaf4 100644 --- a/MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean +++ b/MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean @@ -210,13 +210,10 @@ example : min a b + c = min (a + c) (b + c) := by SOLUTIONS: -/ apply le_antisymm · apply aux - have h : min (a + c) (b + c) = min (a + c) (b + c) - c + c := by rw [sub_add_cancel] - rw [h] - apply add_le_add_left - rw [sub_eq_add_neg] + rw [← add_neg_le_iff_le_add] apply le_trans apply aux - rw [add_neg_cancel_right, add_neg_cancel_right] + repeat rw [add_neg_cancel_right] -- QUOTE. /- TEXT: