case intro
b c : ℤ
⊢ ↑(b * c / b) = ↑(b * c) / ↑b
a b : ℤ
h : b ∣ a
⊢ ↑(a / b) = ↑a / ↑b
rcases h with ⟨c, rfl⟩
no goals
case intro
b c : ℤ
⊢ ↑(b * c / b) = ↑(b * c) / ↑b
rw [mul_comm b, Int.mul_ediv_assoc c (dvd_refl b), Int.cast_mul,
  coe_int_div_self, Int.cast_mul, mul_div_assoc]