α : Type u_1
β : Type ?u.300647
γ : Type ?u.300650
δ : Type ?u.300653
inst✝ : CommMonoid α
a b : Associates α
⊢ a ≤ a * b
α : Type u_1
β : Type ?u.300647
γ : Type ?u.300650
δ : Type ?u.300653
inst✝ : CommMonoid α
a b : Associates α
⊢ a ≤ b * a
rw [mul_comm]
no goals
α : Type u_1
β : Type ?u.300647
γ : Type ?u.300650
δ : Type ?u.300653
inst✝ : CommMonoid α
a b : Associates α
⊢ a ≤ a * b
exact le_mul_right