chore: Nat.mod_succ (#9031)

A simp lemma specialized to `n % n.succ` Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
leanprover-community · Dec 14, 2023 · 1efef4c · 1efef4c
1 parent d2fe557
commit 1efef4c
Showing 1 changed file with 4 additions and 0 deletions.
diff --git 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 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