α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
⊢ a ≤ a * b
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
⊢ a ≤ b * a
rw [mul_comm]
no goals
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
⊢ a ≤ a * b
exact le_self_mul