rw [Nat.add_comm, Nat.lt_iff_add_one_le, Nat.add_assoc]
r : Range
⊢ r.start + (r.stop - r.start + r.step - 1) / r.step * r.step < r.stop + r.step
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step * r.step + (r.start + 1) ≤ r.stop + r.step