R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬b * a ≺ b
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬a * b ≺ b
rw [mul_comm]
no goals
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬b * a ≺ b
exact mul_left_not_lt b h