Deprecate pos-distrib-* in favour of pos-*-commute?

[gallais]

In Data.Integer.Properties,

pos-distrib-* : ∀ x y → (+ x) * (+ y) ≡ + (x ℕ* y)

is the symmetric of the not yet existing function

pos-*-commute : ℕtoℤ.Homomorphic₂ +_ _ℕ*_ _*_

where module ℕtoℤ = Morphism.Definitions ℕ ℤ _≡_.

Names based on the existing function

abs-*-commute : ℤtoℕ.Homomorphic₂ ∣_∣ _*_ _ℕ*_

where module ℤtoℕ = Morphism.Definitions ℤ ℕ _≡_

[mechvel]

I vote for the suggestion by @gallais.
Also pos-*-commute do exist in lib-1.5.
Also even if it is pos-distrib-* then at least the equality parts in the signature need to be swapped.

[jamesmckinna]

But what about the general injunction against spurious additional -commute suffixes, as per issue #509 ?

[JacquesCarette]

So pos-* and abs-* ?