case intro
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a c✝ d c : α
⊢ a ≤ a * c
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
⊢ (∃ c, b = a * c) → a ≤ b
rintro ⟨c, rfl⟩
no goals
case intro
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a c✝ d c : α
⊢ a ≤ a * c
exact le_self_mul