feat(tactic/ring_exp): handle `nat.succ p` as `p + 1` (#5166)
Fixes: #5157
This PR adds a `rewrite` operation to `ring_exp`, which takes a normalized `p' : ex sum` and a proof that `p = p'.orig`, and shows `p` also normalizes to `p'.pretty`. The only use currently is `nat.succ`. If we still had `nat.has_pow`, the same function could have handled rewriting from `nat.has_pow` to `monoid.has_pow`.
