Reconciling `Data.Nat.Divisibility.Core._∣_` and `Algebra.Definitions.RawMagma._∣_`

[jamesmckinna]

The substance of the issue (for the additive fragment of Nat) is already discussed in #1919, but that issue can (should!) be closed by merging #1948. So this is a placeholder to work on this specific problem in the multiplicative fragment of Nat.

Carrying over the summary from #2013:
Two Three parts to this:

• low-hanging fruit: added pattern synonym and consequences/uses of it to Data.Nat.* (merged in Reconciling Data.Nat.Divisibility.Core._∣_ and Algebra.Definitions.RawMagma._∣_ #2013)
• higher-hanging fruit: reconcile the two definitions of _∣_ for the Data.Nat.Base.*-rawMagma instance
• knock-on changes for Data.Integer.Divisibility.* and Data.Rational.* only if the preceding step succeeds

cf. #679

[jamesmckinna]

Picking this up again on the back of #2604.

There seem to be two directions to go in (once again: flip symmetry!)

• redefine Data.Nat.Divisibility.Core._∣_ in terms of Algebra.Definitions.RawMagma *-rawMagma, renaming _,_ to divides, and then having to fix up all the uses in Data.Nat/Data.Integer/Data.Rational uses with appropriate sprinkles of symmetry
• redefine Algebra.Definitions.RawMagma._∣_ to flip the direction of the equality fields, etc.

Personally, I think that the latter is the better course of action, but may cause problems for external clients of stdlib such as @mechvel 's libraries.

TL;DR: heuristic should read

complicated/unknown = simpler/known

However, I think it is the better choice, because of the following refinement of the complicated = simple heuristic which has emerged in writing equations in the library, as discussed elsewhere (I can't remember off the top of my head, but I was the one making the point, about mode of an equation... how do we search GitHub comments for these things?) namely:

• complicated might only appear as a variable name in the stated equation, but it will be used in a context where that variable sis instantiated with an arbitrarily complicated expression... whereas
• simple might be a superficially more complicated RHS expression than the LHS, but is appearing in a 'standard' form. moreover one which instantiates its sub-terms upon application of the relevant lemma.

For divisibility, I'm imagining that we want equality to accept an arbitrary LHS, and then to re-express it on the RHS as a known product of factors. Currently the definitions in Algebra.Definitions.RawMagma._∣_ are the 'wrong way round' for that reading... with a lot of bogus/redundant appeals to sym as a consequence.

[jamesmckinna]

Suggest also, for technical reasons, that we do not export _∣_ as a definition in its own right when observing the convention that, for commutative monoid operations, it be 'taken as read' that it refers to right-divisibility. Rather, in the spirit of reducing module-local cognitive load, that the user should make that choice clear when importing divisibility via a renaming declaration... which makes explicit what is going on 'in place'. cf. some of @JacquesCarette 's and @MatthewDaggitt 's recent comments.

Or else that if we do want to retain the existing convention, that we make it a module definition, rather than a flat type definition, because that plays better with open/renaming etc. of the fields of the associated record on subsequent (possibly qualified) import. Or at least, that how it seems for me when experimenting with these choices... shout-out to @gallais for comment on this in the context of #2604 (it would, of course, be a breaking change, so maybe belongs in a separate PR.

[mechvel]

Please, remain the general _∣_ definition untouched.
My library uses the general _∣_ widely. Its definition has been changed once, respectively this required an effort of me to change much of code. Now you go with the next round. I disliked the first change, and do not understand the reasons for the future one.