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