Adding some sub_emod lemmas to DivModLemmas

Stream: lean4

[Vlad Tsyrklevich]

I had a need for the subtraction equivalents of the (simp) theorems Int.emod_add_emod (a % n + b) % n = (a + b) % n and Int.add_emod_emod (a + b % n) % n = (a + b) % n. lean4 CONTRIBUTING.md indicates I should open a thread for new changes. I'll leave this thread open for a few days and submit these sub lemmas upstream if no one objects!

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

EDIT: Updated code to feedback.

[Dan Velleman]

Int.emod_add_emod m n (-k) proves (m % n - k) % n = (m - k) % n.

[Vlad Tsyrklevich]

Updated! I thought I had tested this, but it must have been only for sub_emod_emod