no goals
a c d : Int
cz : c = 0
⊢ div (a * (c * d)) c = a * div (c * d) c
simp [cz, Int.mul_zero]
no goals
a c d : Int
cz : ¬c = 0
⊢ div (a * (c * d)) c = a * div (c * d) c
rw [Int.mul_left_comm, Int.mul_div_cancel_left _ cz, Int.mul_div_cancel_left _ cz]