rewrite [hd, mul_comm k] at h₂ h₃ ⊢
m k x : ℕ
h₁ : k ∣ m
h₂ : m ≤ x
h₃ : x < m + k
d : ℕ
hd : m = k * d
⊢ x / k * k = m
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