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]

My only nitpick here, in terms of style-guide

agda-stdlib/doc/style-guide.md

Lines 189 to 196 in 5c64117

	* If multiple import modifiers are used, then they should occur in the
	following order: `public`, `using` `renaming`, and if `public` is used
	then the `using` and `renaming` modifiers should occur on a separate line.
	For example:
	```agda
	open Monoid monoid public
	using (ε) renaming (_∙_ to _+_)
	```

is as follows:

Suggested change

	open PM +-monoid using () renaming
	( ε-unique to 0#-unique; ε-comm to 0#-comm
	; elimʳ to +-elimʳ; introʳ to +-introʳ
	; elimˡ to +-elimˡ; introˡ to +-introˡ
	; introᶜ to +-introᶜ
	; cancelʳ to +-cancel-invʳ; insertʳ to +-insertʳ
	; cancelˡ to +-cancel-invˡ; insertˡ to +-insertˡ
	; cancelᶜ to +-cancel-invᶜ; insertᶜ to +-insertᶜ) public
	open PM +-monoid public
	using ()
	renaming ( ε-unique to 0#-unique; ε-comm to 0#-comm
	; elimʳ to +-elimʳ; introʳ to +-introʳ
	; elimˡ to +-elimˡ; introˡ to +-introˡ
	; introᶜ to +-introᶜ
	; cancelʳ to +-cancel-invʳ; insertʳ to +-insertʳ
	; cancelˡ to +-cancel-invˡ; insertˡ to +-insertˡ
	; cancelᶜ to +-cancel-invᶜ; insertᶜ to +-insertᶜ)

plus or minus some additional offset whitespace.

[jamesmckinna]

Ditto.

Suggested change

	open PM *-monoid using () renaming
	( ε-unique to 1#-unique; ε-comm to 1#-comm
	; elimʳ to *-elimʳ; introʳ to *-introʳ
	; elimˡ to *-elimˡ; introˡ to *-introˡ
	; introᶜ to *-introᶜ
	; cancelʳ to *-cancel-invʳ; insertʳ to *-insertʳ
	; cancelˡ to *-cancel-invˡ; insertˡ to *-insertˡ
	; cancelᶜ to *-cancel-invᶜ; insertᶜ to *-insertᶜ) public
	open PM *-monoid public
	using ()
	renaming ( ε-unique to 1#-unique; ε-comm to 1#-comm
	; elimʳ to *-elimʳ; introʳ to *-introʳ
	; elimˡ to *-elimˡ; introˡ to *-introˡ
	; introᶜ to *-introᶜ
	; cancelʳ to *-cancel-invʳ; insertʳ to *-insertʳ
	; cancelˡ to *-cancel-invˡ; insertˡ to *-insertˡ
	; cancelᶜ to *-cancel-invᶜ; insertᶜ to *-insertᶜ)