rewrite [← Nat.div_div_eq_div_mul]
n m k d x : ℕ
h₂ : x + 1 ∣ m
hd : m = (x + 1) * d
⊢ n / (x + 1) * (x + 1) / ((x + 1) * d) = n / ((x + 1) * d)
n m k d x : ℕ
h₂ : x + 1 ∣ m
hd : m = (x + 1) * d
⊢ n / (x + 1) * (x + 1) / (x + 1) / d = n / ((x + 1) * d)