rewrite [Nat.sub_one, Nat.mul_pred_left]
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x * d - x = (d - 1) * x
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x * d - x = d * x - x