ConstraintAnalysis: Use spans to prove things (#9025)

When two constraints can be expressed as spans, see if one shows the
other is true or not.

Landing this requires improving something else, otherwise tests would
regress: we "got lucky" before and did not notice that `x >= 0` was
always true when unsigned, so we carried that around, and after `x++`
it turned into `x >= 1` which is no longer trivial. We do need that latter
constraint, so add the following rule: when `x++` and `x` does not
overflow during that addition (as proven by some bound like `x < 10`)
then we can add `x > 0` (since it can no longer be 0 due to the `x++`).