Some properties of unnormalised rationals are named inconsistently

[SlimTim10]

Compare

agda-stdlib/src/Data/Rational/Unnormalised/Properties.agda

Line 1251 in eb9615d

*-monoˡ-≤-nonNeg : ∀ r .{{_ : NonNegative r}} → (_* r) Preserves _≤_ ⟶ _≤_

to

agda-stdlib/src/Data/Rational/Properties.agda

Line 1342 in eb9615d

*-monoˡ-≤-nonNeg : ∀ r .{{_ : NonNegative r}} → (r *_) Preserves _≤_ ⟶ _≤_

*-monoˡ-≤-nonNeg should be swapped with *-monoʳ-≤-nonNeg. Same for a few others nearby.

[jamesmckinna]

This is a duplicate of the still-open #1579 ... cf. #1436 and related PRs... still a mess I'm afraid after all these years, and because fixing it would be a non-trivial breaking change, it's only going to be tackled in v3.0... :-(