mathlib3

6e8c150a - feat(data/nat/basic): add recursion principle `even_odd_rec` as a wrapper around `binary_rec` (#15457)

feat(data/nat/basic): add recursion principle `even_odd_rec` as a wrapper around `binary_rec` (#15457) This is just a wrapper around `nat.binary_rec`, so that the subsequent reasoning after invoking this recursion principle can remain in the familiar world of `ℕ` and avoids having to switch to dealing with `bit0` and `bit1`. Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>