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 ℤ ℕ _≡_