Tactic for solving equations in the language of additive, commutative monoids and groups. This version of abel fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.

Tactic for solving equations in the language of additive, commutative monoids and groups. Attempts to prove the goal outright if there is no at specifier and the target is an equality, but if this fails it falls back to rewriting all monoid expressions into a normal form.