rw [Nat.div_mul_cancel h.2.2]
r : Range
x : ℕ
h : r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
⊢ r.start + (x - r.start) / r.step * r.step = x
r : Range
x : ℕ
h : r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
⊢ r.start + (x - r.start) = x