feat: add Int.emod_sub_emod and Int.sub_emod_emod

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

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