Commit 2021-06-19 08:22 2ca04524
View on Github →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