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