rw [Nat.div_eq_zero_iff r.step_pos,
    Nat.lt_iff_add_one_le,
    Nat.sub_add_cancel]
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step = 0 ↔ r.start = r.stop
r : Range
⊢ r.stop - r.start + r.step ≤ r.step ↔ r.start = r.stop

r : Range
⊢ 1 ≤ r.stop - r.start + r.step