feat(data/nat/parity,data/int/parity): odd numbers (#4357)
As discussed at
<https://leanprover.zulipchat.com/#narrow/stream/208328-IMO-grand-challenge/topic/formalizing.20IMO.20problems>,
define `nat.odd` and `int.odd` to allow a more literal expression
(outside of mathlib; for example, in formal olympiad problem
statements) of results whose informal statement refers to odd numbers.
These definitions are not expected to be used in mathlib beyond the
`simp` lemmas added here that translate them back to `¬ even`. This
is similar to how `>` is defined but almost all mathlib results are
expected to use `<` instead.
It's likely that expressing olympiad problem statements literally in
Lean will end up using some other such definitions, where avoiding API
duplication means almost everything relevant in mathlib is developed
in terms of the expansion of the definition.
