[ add ] rule of signs for RingWithoutOne

[jamesmckinna]

Surprised to find this was not anywhere in the library!
Warm-up for tackling #2704 , so could instead be folded into a PR for that, but this is of independent interest/importance?

Took the liberty of using the PR also to do some tidying up of the module... and to fix the markup in CHANGELOG

... prompting me to revisit #1875 : I'd still push for deprecating x+x≈x⇒x≈0 in favour of +-identityˡ-unique, otherwise if we think this lemma important enough, then perhaps it should be re-exported from where it's first definable, namely all the way up (down?) the hierarchy in Algebra.Loop.Properties...

[jamesmckinna]

A general point about Algebra.Properties.X vs. Algebra.Consequences.Setoid: should this lemma be in Properties.RingWithoutOne, or proved first in Consequences, for a longish list of hypotheses?

[JacquesCarette]

A general point about Algebra.Properties.X vs. Algebra.Consequences.Setoid: should this lemma be in Properties.RingWithoutOne, or proved first in Consequences, for a longish list of hypotheses?

I'm thinking Properties.RingWithoutOne. The only reason I would put it in Consequences is if the proof uses a 'weird' set of properties that amounts to an algebra without a name that is unlikely to see much use if it were created.

[MatthewDaggitt]

In the interest of getting a release out, I'm bumping this to v2.4