no goals
a b c : Int
az : a = 0
⊢ div (a * b) a ∣ div (a * b * c) a
simp [az]
a b c : Int
az : ¬a = 0
⊢ b ∣ b * c
a b c : Int
az : ¬a = 0
⊢ div (a * b) a ∣ div (a * b * c) a
rw [Int.mul_div_cancel_left _ az, Int.mul_assoc, Int.mul_div_cancel_left _ az]
no goals
a b c : Int
az : ¬a = 0
⊢ b ∣ b * c
apply Int.dvd_mul_right