From 78ed072ab0191391e2f2673907e741e5a0a98327 Mon Sep 17 00:00:00 2001
From: Vlad Tsyrklevich <vlad902@gmail.com>
Date: Wed, 8 Jan 2025 03:20:43 +0100
Subject: [PATCH] feat: add `Int.emod_sub_emod` and `Int.sub_emod_emod` (#6507)

This PR adds the subtraction equivalents for `Int.emod_add_emod` (`(a %
n + b) % n = (a + b) % n`) and `Int.add_emod_emod` (`(a + b % n) % n =
(a + b) % n`). These are marked @[simp] like their addition equivalents.

Discussed on Zulip in

https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Adding.20some.20sub_emod.20lemmas.20to.20DivModLemmas
---
 src/Init/Data/Int/DivModLemmas.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index d0c86c5c98..b8f121043a 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -534,6 +534,13 @@ theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
 @[simp] theorem emod_emod (a b : Int) : (a % b) % b = a % b := by
   conv => rhs; rw [← emod_add_ediv a b, add_mul_emod_self_left]
 
+@[simp] theorem emod_sub_emod (m n k : Int) : (m % n - k) % n = (m - k) % n :=
+  Int.emod_add_emod m n (-k)
+
+@[simp] theorem sub_emod_emod (m n k : Int) : (m - n % k) % k = (m - n) % k := by
+  apply (emod_add_cancel_right (n % k)).mp
+  rw [Int.sub_add_cancel, Int.add_emod_emod, Int.sub_add_cancel]
+
 theorem sub_emod (a b n : Int) : (a - b) % n = (a % n - b % n) % n := by
   apply (emod_add_cancel_right b).mp
   rw [Int.sub_add_cancel, ← Int.add_emod_emod, Int.sub_add_cancel, emod_emod]