a b c : ℤ
habc : a ∣ c * b
hab : gcd a b = 1
⊢ a ∣ c
a b c : ℤ
habc : a ∣ b * c
hab : gcd a b = 1
⊢ a ∣ c
rw [mul_comm] at habc
no goals
a b c : ℤ
habc : a ∣ c * b
hab : gcd a b = 1
⊢ a ∣ c
exact dvd_of_dvd_mul_left_of_gcd_one habc hab