i : Nat
r : Std.Range
h : r.start ≤ i ∧ i < r.stop
⊢ i < r.stop
i : Nat
r : Std.Range
h : i ∈ r
⊢ i < r.stop
simp [Membership.mem] at h
no goals
i : Nat
r : Std.Range
h : r.start ≤ i ∧ i < r.stop
⊢ i < r.stop
exact h.2