Use strict inequalities in relational witness invariants

In #1849 our relational domains produce a witness invariant
```c
(long long )i >= (long long )\at(i, AnyPrev) + 1LL
```
This is a transition invariant, but that's actually beside the point.

Instead of outputting `i >= j + 1` we could output `i > j`, knowing that we're working with integers.