Ring reasoning

[JacquesCarette]

Reasoning combinators for monoid, renamed and adapted for Ring. Builds on #2692 .

[Taneb]

1. I'd like to see the new semigroup properties here as well
2. The semigroup properties on * and the monoid properties on + work for RingWithoutOne
3. In fact, they work on Semiring and SemiringWithoutOne, but we don't have a Properties module for those

[jamesmckinna]

@Taneb 's 1,2,3 above echo my thoughts on looking at these, but maybe, given our ongoing issues regarding naming in #2688 that it isn't so straightforward to back-fill the Properties for weaker structures... yet?

[jamesmckinna]

Thanks for incorporating my nitpick suggestions.

[jamesmckinna]

Guessing that this PR hints that we should perhaps also have/need the intermediate extension to Algebra.Properties.(Abelian)Group to incorporate inverse equational simplification for the +-abelianGroup sub-structure/-bundle... as a downstream PR.

[JacquesCarette]

Yes, there is quite a lot that can be done in this vein.

We should be careful not to have perfect be the enemy of definite-improvement...

[jamesmckinna]

Yes, there is quite a lot that can be done in this vein.

We should be careful not to have perfect be the enemy of definite-improvement...

Yeah, not my intention at all to obstruct this PR with demands for more here... but elsewhere, in due course, definitely!

[JacquesCarette]

I guess, strictly speaking, neither you nor @Taneb are blocking this on requiring more features...

[jamesmckinna]

Absolutely not blocking from me!

but... maybe a rebase against the new master to sort out the CHANGELOG conflict, and to catch the already-merged Semigroup commits (I think the Monoid PR I still open though...?)?

[JacquesCarette]

That's why it's Draft, I need to do at least those changes.