apply Nat.add_le_of_le_sub
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step * r.step + (r.start + 1) ≤ r.stop + r.step
case hle
r : Range
⊢ r.start + 1 ≤ r.stop + r.step

case h
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step * r.step ≤ r.stop + r.step - (r.start + 1)