Proposal with ∣quot and ∣eq for _∣_

[mechvel]

Algebra.Definitions.RawMagma defines

_∣_ :  Rel A (a ⊔ ℓ)                                                              
x ∣ y =  ∃ λ q → (q ∙ x) ≈ y                                                      

(here I omit the upper index ʳ).
This provokes applying proj₁, proj₂ to extract the quotient and the equality proof from d : x ∣ y.
To support a better style, it has sense to introduce to standard the functions to extract these parts:

∣quot :  ∀ {x y} → x ∣ y → A 
∣quot = proj₁

∣eq :  ∀ {x y} → (d : x ∣ y) → (x ∙ (∣quot d)) ≈ y 
∣eq d = proj₂ d

(the upper indices ʳ ... in _∣_ to be treated respectively).
?

[MatthewDaggitt]

It might be better simply to turn this into a record with suitable names for the fields...

[mechvel]

But the generic _∣_ is already defined in lib-1.7 in Algebra.Definitions.RawMagma as

x ∣ʳ y =  ∃ λ q → (q ∙ x) ≈ y        -- Gen-1.7
_∣_ =  _∣ʳ_

The proposed functions ∣quot and ∣eq preserve the backwards compatibility.
How widely this Gen-1.7 from RawMagma is used in lib-1.7 ?

On the other hand, lib-1.7 has in Data.Nat.Divisibility.Core:

record _∣_ (m n : ℕ) :  Set where                    -- Nat-1.7                                                  
  constructor divides                                                             
  field quotient : ℕ                                                              
         equality : n ≡ quotient * m                                               

Its generalization could be set to Algebra.Definitions.RawMagma as

record _∣_ (x y : A) :  Set where           -- Gen-2.0                               
  constructor divides                                                             
  field quotient :  A 
         equality  :  (quotient ∙ x)  ≈ y       -- (the equality sides are swapped)

together with the versions of _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_ for the left and right divisibility,
and to replace the existing definition of _∣_.
As to me, I am ready to use this Gen-2.0 version.
If so then, please, let (x ∣ y) be as (quotient ∙ x) ≈ y
(this is you who have insisted on this).

If yes, then the next question will be: what to do with the existing divisibility definitions for Nat and Integer.
It is desirable for them to import the generic _∣_ and to use the proofs for *-commutativeMonoid and
cancellativeCommutativeSemiring,
and the generic notions of Irreducible, Prime, Coprime (which are in lib-1.7).
The same is for GCD, but I failed to push its properties implementation to Standard, it remains in my applied
program.