From 8bbf21e7e6d56693fd6e1d57633cc3892bdcb332 Mon Sep 17 00:00:00 2001 From: Yakov Pechersky Date: Wed, 13 Dec 2023 16:28:41 -0500 Subject: [PATCH 1/2] chore: Nat.mod_succ A simp lemma specialized to `n % n.succ` --- Mathlib/Data/Nat/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean index 26d9f8dd4fb27..62282ba88bb69 100644 --- a/Mathlib/Data/Nat/Basic.lean +++ b/Mathlib/Data/Nat/Basic.lean @@ -741,6 +741,10 @@ theorem mod_succ_eq_iff_lt {a b : ℕ} : a % b.succ = a ↔ a < b.succ := mod_eq_iff_lt (succ_ne_zero _) #align nat.mod_succ_eq_iff_lt Nat.mod_succ_eq_iff_lt +@[simp] +theorem Nat.mod_succ (n : ℕ) : n % n.succ = n := + Nat.mod_eq_of_lt (Nat.lt_succ_self _) + -- Porting note `Nat.div_add_mod` is now in core. theorem mod_add_div' (m k : ℕ) : m % k + m / k * k = m := by From 3dd42e13bbb47bf7c7de08fd7611800b5eaccff2 Mon Sep 17 00:00:00 2001 From: Yakov Pechersky Date: Wed, 13 Dec 2023 17:51:24 -0500 Subject: [PATCH 2/2] Update Mathlib/Data/Nat/Basic.lean --- Mathlib/Data/Nat/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean index 62282ba88bb69..69fecd7a3760d 100644 --- a/Mathlib/Data/Nat/Basic.lean +++ b/Mathlib/Data/Nat/Basic.lean @@ -742,7 +742,7 @@ theorem mod_succ_eq_iff_lt {a b : ℕ} : a % b.succ = a ↔ a < b.succ := #align nat.mod_succ_eq_iff_lt Nat.mod_succ_eq_iff_lt @[simp] -theorem Nat.mod_succ (n : ℕ) : n % n.succ = n := +theorem mod_succ (n : ℕ) : n % n.succ = n := Nat.mod_eq_of_lt (Nat.lt_succ_self _) -- Porting note `Nat.div_add_mod` is now in core.