max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add @[simp] to Nat.sub_add_cancel (#3378)

Browse source
This commit is contained in:
Scott Morrison 2024-02-18 17:48:10 +11:00 • committed by GitHub
parent d569ed4e5f
commit e206e53f4e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/Nat/Basic.lean
View file

@ -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