feat(data/{fin,nat,zmod}): prove `zmod.coe_add_eq_ite` (#7975)
This PR adds a couple of lemmas relating addition modulo `n` (in `ℕ`, `fin n` or `zmod n`) and addition in `ℕ` or `ℤ`.
[Based on this Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Homomorphism.20from.20the.20integers.20descends.20to.20.24.24.5Cmathbb.7BZ.7D.2Fn.24.24)
