ยง Correctness of lower_bound search with half-open intervals

// precondition: `xs` is sorted.
// find rightmost i such that xs[i] <= y and dp[i+1] > y.
int tallest(vector<long> &xs, int y) {
    // [l, r)
    int l = 0, r = dp.size();
    // precondition: l < r
    while(1) {
        if (l + 1 == r) { return l; }
        // info gained from if: r > (l+1)
        int m = (l+r)/2;
        // should this be (xs[m] > y) or (xs[m] >= y)?
        if (xs[m] > y) {
            r = m; // will decrease interval floor division.
        } else {
            // r > (l+1)
            // so m := (l+r/2) > (2l+1)/2 > l.
            l = m;
        }
    }
}
// precondition: `xs` is sorted.
// find i such that xs[i] <= y and dp[i+1] > y.
int tallest(vector<long> &xs, int y) {
    // [l, r)
    int l = 0, r = dp.size();
    // precondition: l < r
    while(1) {
        if (l + 1 == r) { return l; }
        // info gained from if: r > (l+1)
        int m = (l+r)/2;
        // should this be (xs[m] > y) or (xs[m] >= y)?
        if (xs[m] > y) {
            // move interval towards `l` for smaller values.
            r = m; // will decrease interval floor division.
        } else if (xs[m] < y) {
            // move interval towards `r` for larger values.
            // r > (l+1)
            // so m := (l+r/2) > (2l+1)/2 > l.
            l = m;
        } else {
            //xs[m] == y
            // we want rightmost index `l` where `xs[l] <= y`.
            // - this `xs[m]` is a legal index.
            // - we want rightmost `m`. Since `m > l`, move `l` rightward by setting `l = m`.
            l = m;
        }
    }
}