no goals
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
az : a = 0
⊢ a * b / a ∣ a * b * c / a
simp [az]
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
az : ¬a = 0
⊢ b ∣ b * c
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
az : ¬a = 0
⊢ a * b / a ∣ a * b * c / a
rw [Int.mul_ediv_cancel_left _ az, mul_assoc, Int.mul_ediv_cancel_left _ az]
no goals
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
az : ¬a = 0
⊢ b ∣ b * c
apply dvd_mul_right