rw [mul_comm]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ v nav b ≤ v nav (a * b)
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ v nav b ≤ v nav (b * a)