rewrite [← Nat.succ_mul] at h₃
m k x : ℕ
h₁ : k ∣ m
d : ℕ
h₃ : x < d * k + k
h₂ : d * k ≤ x
hd : m = k * d
⊢ x / k * k = d * k
m k x : ℕ
h₁ : k ∣ m
d : ℕ
h₃ : x < Nat.succ d * k
h₂ : d * k ≤ x
hd : m = k * d
⊢ x / k * k = d * k