Commit 2020-05-09 14:34 e1192f35

feat(data/nat/basic): add mod_add_mod and add_mod_mod (#2635) Added the mod_add_mod and add_mod_mod lemmas for data.nat.basic. I copied them from data.int.basic, and just changed the data type. Would there be issues with it being labelled @[simp]? Also, would it make sense to refactor add_mod above it to use mod_add_mod and add_mod_mod? It'd make it considerably shorter. (Tangential note, there's a disparity between the mod lemmas for nat and the mod lemmas for int, for example int doesn't have add_mod, should that be added in a separate PR?)