 Lower-bound binary search invariant

In a nondecreasing array, the first position whose entry is at least $x$ is found by maintaining a half-open unresolved interval $[l,h)$. Entries before $l$ are smaller than $x$; entries from $h$ onward are at least $x$. Initially $l=c_0,h=c_1$. At midpoint $m$, replace $l$ by $m+1$ if $A[m]<x$, and otherwise replace $h$ by $m$. Monotonicity preserves the loop invariant, and $h-l$ decreases. On exit $l=h$ is the first qualifying position, or $c_1$ if no such entry exists. Repeated values and endpoint cuts require no additional case.