Membership.get_elem_helper

theorem Membership.get_elem_helper : ∀ {i n : ℕ} {r : Std.Range}, i ∈ r → r.stop = n → i < n

This theorem, "Membership.get_elem_helper", states that for any natural numbers `i` and `n`, and any standard range `r`, if `i` is an element of `r` and the stop value of `r` is `n`, then `i` is less than `n`. In simpler terms, it means any element of a specified range is less than the upper boundary of that range.

More concisely: For any natural number `i`, if `i` is an element of a standard range `r` with stop value `n`, then `i` < `n`.