match k with
| 0 => rw [Nat.mul_zero, Nat.zero_mul, Nat.zero_div, Nat.div_zero]
| x + 1 =>
  rewrite [← Nat.div_div_eq_div_mul]
  rewrite [Nat.mul_div_cancel _ (Nat.add_pos_right _ zero_lt_one)]
  exact Nat.div_div_eq_div_mul _ _ _
n m k : ℕ
h₂ : k ∣ m
d : ℕ
hd : m = k * d
⊢ n / k * k / (k * d) = n / (k * d)
no goals