Theorem: LeanColls.Range.nth_size_eq_stop (LeanColls/Data/Range.lean)

State before:
r : Range
h : r.step = 1
⊢ r.nth r.size = r.stop
Tactic:
simp [nth, size, h]
State after:
no goals