For example, we can fold `x - 1 < x` -> `true`, if we can prove that `x - 1` does not overflow.

This is a very common pattern:

```
for (i = 0; i < arr.length; ++i) {
  foo(arr[i])
}
```

We hoist out loop predicate:
```
if (arr.length - 1 >= arr.length) { trap(); }
for (i = 0; i < arr.length; ++i) {
  foo(arr[i])
}
```

We know `arr.length - 1` never overflows because `arr.length` is non-negative. We can fold away that check.