Open Algebra.Properties.AbelianGroup for addition in Data.{Integer,Rational}.Properties

[Taneb]

trafficstars

It contains a lot of properties that I keep reaching for but not finding, that we can add to those modules basically for free.

It might also be worth making a module Algebra.Properties.CommutativeRing etc. combining Algebra.Properties.AbelianGroup and Algebra.Properties.CommutativeMonoid with more ring-ish names, plus giving us a home for any ring-specific properties we think of

[MatthewDaggitt]

Yup, that sounds reasonable. See the following example where we do something similar:

https://github.com/agda/agda-stdlib/blob/95270b78d8d6ded67fcdf94095a056a0245de547/src/Data/Rational/Properties.agda#L1391