simp [nth, size, Nat.lt_iff_add_one_le,
      Nat.le_div_iff_mul_le r.step_pos]
r : Range
i : ℕ
⊢ r.nth i < r.stop ↔ i < r.size
r : Range
i : ℕ
⊢ r.start + i * r.step + 1 ≤ r.stop ↔ (i + 1) * r.step ≤ r.stop - r.start + r.step - 1