rw [Nat.add_comm, Nat.sub_add_eq,
    Nat.add_sub_assoc r.start_le_stop,
    Nat.add_comm,
    Nat.add_sub_assoc r.step_pos]
case h.e'_4
r : Range
⊢ r.stop + r.step - (r.start + 1) = r.stop - r.start + r.step - 1
no goals