α : Type u_1
inst✝ : CommSemigroup α
a b c✝ : α
h : a ∣ b
c : α
⊢ a ∣ b * c
α : Type u_1
inst✝ : CommSemigroup α
a b c✝ : α
h : a ∣ b
c : α
⊢ a ∣ c * b
rw [mul_comm]
no goals
α : Type u_1
inst✝ : CommSemigroup α
a b c✝ : α
h : a ∣ b
c : α
⊢ a ∣ b * c
exact h.mul_right _