feat(tactic/norm_num): new all-lean norm_num (#2589)
This is a first draft of the lean replacement for `tactic.norm_num` in core. This isn't completely polished yet; the rest of `norm_num` can now be a little less "global-recursive" since the primitives for e.g. adding and multiplying natural numbers are exposed.
I'm also trying out a new approach using functions like `match_neg` and `match_numeral` instead of directly pattern matching on exprs, because this generates smaller (and hopefully more efficient) code. (Without this, some of the matches were hitting the equation compiler depth limit.)
I'm open to new feature suggestions as well here. `nat.succ` and coercions seem useful to support in the core part, and additional flexibility using `def_replacer` is also on the agenda.
