Add certain proofs for ``_∤_``

[mechvel]

I suggest to add to Algebra.Definitions.RawMagma the proofs for _∤_ which are similar to the proofs ∣-respʳ, ∣-respˡ, ∣-resp . For example, like this:

∤-respˡ  :  {x : C} →  (_∤ x) Respects _≈_
∤-respˡ y≈y' y∤x y'∣x =  y∤x y∣x      where
                                      y∣x = ∣-respˡ (sym y≈y') y'∣x
∤-respʳ :  {x : C} → (x ∤_) Respects _≈_
∤-respʳ = ...

∤-resp  :   _∤_  Respects₂  _≈_
∤-resp  =  ...

Otherwise almost everyone who programs algebra would have to implement them oneself.

[MatthewDaggitt]

They can't live in Algebra.Definitions.RawMagma as you don't have a proof that the relation is an equality.

Instead these already exist in Algebra.Properties.Magma.Divisibility:

https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Properties/Magma/Divisibility.agda

[mechvel]

I do not see these lemmas in Algebra.Properties.Magma.Divisibility in lib-2.0. Do you mean that they have to appear in the next official version?

[MatthewDaggitt]

No, they exist in v2.0 as well:

https://github.com/agda/agda-stdlib/blob/v2.0/src/Algebra/Properties/Magma/Divisibility.agda

[mechvel]

I see there that _∤_ is imported, but I do not see there the three suggested proofs

∤-resp  :   _∤_  Respects₂  _≈_
...

For any occasion: the last nonempty line in this file is of number 54.

[MatthewDaggitt]

Lines 26-33

[mechvel]

These lines concern _∣_ - divisibility. And I talk about _∤_ - negation of divisibility. Are you saying that ∣-respʳ is also a proof for _∤_ Respectsʳ _≈_ ? (I think, it is not). Or may be your GitHub editor does not show the symbol ∤ ("does not divide") correctly?

[MatthewDaggitt]

Ah sorry, yes my mistake, these are indeed missing and should be added just below.