From e206e53f4e37ecd810b2de36b7544240d579c535 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 18 Feb 2024 17:48:10 +1100 Subject: [PATCH] chore: add @[simp] to Nat.sub_add_cancel (#3378) --- src/Init/Data/Nat/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 9f4d592f36..77c245dd9c 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -621,7 +621,7 @@ theorem add_sub_of_le {a b : Nat} (h : a ≤ b) : a + (b - a) = b := by have : a ≤ b := Nat.le_of_succ_le h rw [sub_succ, Nat.succ_add, ← Nat.add_succ, Nat.succ_pred hne, ih this] -protected theorem sub_add_cancel {n m : Nat} (h : m ≤ n) : n - m + m = n := by +@[simp] protected theorem sub_add_cancel {n m : Nat} (h : m ≤ n) : n - m + m = n := by rw [Nat.add_comm, Nat.add_sub_of_le h] protected theorem add_sub_add_right (n k m : Nat) : (n + k) - (m + k) = n - m := by