have hdvd' : d ∣ (d - 1) * x := Nat.dvd_trans hdvd (Nat.dvd_mul_left _ _)
x d : ℕ
hpos : 0 < d
hdvd : d ∣ 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 - 1) * x / d