Use strict inequalities in relational witness invariants

[sim642]

In #1849 our relational domains produce a witness invariant

(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.