mathlib

57035e18 - chore(data/nat/basic): reorder arguments to `nat.even_odd_rec` to make it work with `induction` (#17165)

chore(data/nat/basic): reorder arguments to `nat.even_odd_rec` to make it work with `induction` (#17165) The `induction` tactic needs `n` to come after `p`. At any rate, the convention is to take `n` last for `*_rec` and first for `*_rec_on`. With this change, `induction n using nat.even_odd_rec` both works and introduces hypotheses with sensible names.