pos-+-commute vs pos-distrib-* in lib-1.5

[mechvel]

Data.Integer.Properties declares

pos-+-commute : ℕtoℤ.Homomorphic₂ +_ ℕ._+_ _+_
...
pos-distrib-* : ∀ x y → (+ x) * (+ y) ≡ + (x ℕ.* y) 

Probably the latter needs to be

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

-- to follow the format of "something distributes over _*_".
Or may be

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

-- to follow the format of pos-+-commute.
?

[gallais]

Is this #501?

[mechvel]

Yes,
withdraw this my issue, please.
I vote for #501.