These lemmas aren't really proved any faster using units, and I will soon need them not to be proved using units.

Part of #9411

These lemmas can actually be proved much earlier than they were.

Part of #9411

`Data.Int.Basic` is currently made of two things:
* Basic lemmas that continue the theory in Std (and could belong there, really)
* Basic algebraic order instances

I need the first ones earlier in the algebraic order hierarchy, hence the split.

Part of #9411

These lemmas aren't really proved any faster using units, and I will soon need them not to be proved using units.

Part of #9411

These lemmas can actually be proved much earlier than they were.

Part of #9411

… their own files

Part of #9411

The first versions for ordered semirings do not need to import so much but:
* they have no obvious place to go
* nobody needs them that early (in particular, it seems nobody needs them without also needing the ordered field version)

Part of #9411

Part of #9411

This allows more files to not depend on `Algebra.GroupPower.Lemmas`, which will soon stop existing.

Part of #9411

The current design for `abs` is flawed:
* The `Abs` notation typeclass has exactly two instances: one for `[Neg α] [Sup α]`, one for `[Inv α] [Sup α]`. This means that:
  * We can't write a meaningful hover for `Abs.abs`
  * Fields have two `Abs` instances!
* We have the multiplicative definition but:
  * All the lemmas in `Algebra.Order.Group.Abs` are about the additive version.
  * The only lemmas about the multiplicative version are in `Algebra.Order.Group.PosPart`, and they get additivised to duplicates of the lemmas in `Algebra.Order.Group.Abs`!

This PR changes the notation typeclass with two new definitions (related through `to_additive`): `mabs` and `abs`. `abs` inherits the `|a|` notation and `mabs` gets `|a|ₘ` instead.

The first half of `Algebra.Order.Group.Abs` gets multiplicativised. A later PR will multiplicativise the second half,  and another one will deduplicate the lemmas in `Algebra.Order.Group.PosPart`.

Part of #9411.




Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

These lemmas can be proved much earlier with little to no change to their proofs.

Part of #9411

This changes the typeclass notation approach with plain functions.

Followup to #9553. Part of #9411

These lemmas can be proved earlier.

Part of #9411

These can be defined earlier for free.

Part of #9411

These lemmas can be proved earlier.

Part of #9411




Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

These can be defined earlier for free.

Part of #9411