feat: add Nat.mod_eq_sub and fix dependencies from Nat.sub_mul_eq_mod_of_lt_of_le

[luisacicolini]

This PR adds theorem mod_eq_sub, makes theorem sub_mul_eq_mod_of_lt_of_le not private anymore and moves its location within the rotate* section to use it in other proofs.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9cf83706e743debb47f3b1a48e1b92210c1c0720 --onto 72e952eadc6a171310f1d8e9d6e78acf98421494. (2024-11-21 19:11:18)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9cf83706e743debb47f3b1a48e1b92210c1c0720 --onto 884a9ea2ff70bb4d0c6da4a1c23ffc26c3a974ee. (2024-11-25 08:57:09)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9cf83706e743debb47f3b1a48e1b92210c1c0720 --onto 9a17919ef11c2dba824498229633b8333a0b53d9. (2024-11-26 11:54:24)

[luisacicolini]

Thanks a lot @kim-em @bollu for the reviews! It took me some time to understand it, but the proof of mod_eq_sub_of_le_of_lt should now be okay.

[luisacicolini]

awaiting-reviews

[luisacicolini]

Actually, it looks like one such theorem exists already: Nat.sub_mul_eq_mod_of_lt_of_le so I guess this PR is not needed after all and I can use the other theorem. And maybe move the private theorem to Nat.

[kim-em]

Could we make sure

theorem mod_eq_sub (x w : Nat) : x % w = x - w * (x / w) := by
  conv => rhs; congr; rw [← mod_add_div x w]
  simp

makes it in? Either strip this PR down to just that, or close this PR and include it in a subsequent PR?

[luisacicolini]

I have fixed the dependencies from the existing theorem (which is now not private anymore and in a different location, otherwise I could not use it) and kept mod_eq_sub. Happy to split the PR into two if that is better.