feat(tactic/noncomm_ring): expand out powers using pow_succ

[pechersky]

Somehow, a previous commit broke noncomm_ring. This PR adds some more pow_succ power to it to revive it.

---

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/noncomm_ring.20regression

[pechersky]

Mario Carneiro: I'm not a fan of heuristic extensions to tactics with a well defined scope
Mario Carneiro: a ^ b.succ is not a ring expression
Mario Carneiro: it sounds like you want noncomm_ring_exp

Closing due to feature creep.