apply Nat.eq_of_mul_eq_mul_right hpos
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x - x / d = (d - 1) * x / d
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ (x - x / d) * d = (d - 1) * x / d * d