Investigate solver for Ab-categories/ringoids

[plt-amy]

We know how to solve equations in a ring, and we know how to solve equations in a category. Can we somehow combine them, to solve equations in a ringoid? This would essentially be a way of getting rid of annoying distributivity, associativity, identity and zero goals.

Bonus points if we can somehow make the solver involve the word "polynomialoid".

[TOTBWF]

Tbh this is almost easier than (commutative) rings, as we don't need to worry about any sort of commutation of composition when designing our normal forms.