feat(data/nat,data/int): add some modular arithmetic lemmas (#2460)
These lemmas (a) were found useful in formalising solutions to some
olympiad problems, see
<https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Some.20olympiad.20formalisations>;
(b) seem more generally relevant than to just those particular
problems; (c) do not show up through library_search as being already
present.