Defining `left - 1` to be green `right` to be red can be thought of as "padding" the input to ensure that there is at least one green and one red, but I'll concede that it is sneaky.

(A less sneaky version is to explicitly define new predicates: `is_green2(i) := (i == left - 1) || is_green(i)` and `is_red2(i) := (i == right) || is_red(i)`, where `left` and `right` refer to the function's original parameters (inclusive-exclusive). These predicates can be used as the invariants, and are sufficient for showing that at the end of the loop the result is either the first red, or one-past-the-end if everything is green.)

An alternative is to tweak the invariants:

Let `left` and `right` be the function's original parameters (inclusive-exclusive), and let `l` (that's a lowercase L) and `r` be the variables used in the loop (exclusive-exclusive).

The original invariants are `is_green(l)` and `is_red(r)`, which require sneaky definitions when `l = left - 1` and `r = right`.

The tweaked invariants are `is_green(i) for all i where left <= i <= l` and `is_red(i) for all i where r <= i < right`. In other words, everything up to and including `l` is green, and everything from `r` onward is red.

These invariants are vacuously true when `l = left - 1` and `r = right`, so they hold before the loop (without having to define `left - 1` to be green and `right` to be red).